Changeset 1407
 Timestamp:
 Oct 19, 2011, 11:17:21 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.24.3/reports/D43.tex
r1406 r1407 300 300 \end{lstlisting} 301 301 302 The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register: 302 303 \begin{lstlisting} 303 304 record more_sem_params (p:params_): Type[1] := … … 320 321 }. 321 322 \end{lstlisting} 322 323 \begin{lstlisting} 324 record sem_params: Type[1] := 325 { 326 spp :> params_; 327 more_sem_pars :> more_sem_params spp 328 }. 329 \end{lstlisting} 330 323 For instance, \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively. 324 Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language. 325 Here \texttt{framesT} is the type of stack frames. 326 327 We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}: 331 328 \begin{lstlisting} 332 329 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] := 333 330 { 334 331 more_sparams1 :> more_sem_params p; 335 fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals); 336 fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address); 337 result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p)); 338 init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1; 339 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)); 340 pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1))); 341 fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val); 342 set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)); 343 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))) 332 fetch_statement: 333 genv … p → state (mk_sem_params … more_sparams1) → 334 res (joint_statement (mk_sem_params … more_sparams1) globals); 335 ... 336 save_frame: 337 address → nat → paramsT … p → call_args p → call_dest p → 338 state (mk_sem_params … more_sparams1) → 339 res (state (mk_sem_params … more_sparams1)); 340 pop_frame: 341 genv globals p → state (mk_sem_params … more_sparams1) → 342 res ((state (mk_sem_params … more_sparams1))); 343 ... 344 set_result: 345 list val → state (mk_sem_params … more_sparams1) → 346 res (state (mk_sem_params … more_sparams1)); 347 exec_extended: 348 genv globals p → extend_statements (mk_sem_params … more_sparams1) → 349 succ p → state (mk_sem_params … more_sparams1) → 350 IO io_out io_in (trace × (state (mk_sem_params … more_sparams1))) 344 351 }. 345 352 \end{lstlisting} 346 353 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. 354 355 We bundle \texttt{params} and \texttt{sem\_params} together into a single record. 356 This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language: 347 357 \begin{lstlisting} 348 358 record sem_params2 (globals: list ident): Type[1] := … … 352 362 }. 353 363 \end{lstlisting} 354 364 \noindent 355 365 The \texttt{state} record holds the current state of the interpreter: 356 366 \begin{lstlisting} … … 373 383 ... 374 384 \end{lstlisting} 375 We examine the type of this function 385 We examine the type of this function. 386 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. 387 Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}. 388 Further, the function returns a new state, updated by the single step of execution of the program. 389 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. 376 390 377 391 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 385 399 Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state. 386 400 401 A monad can be characterised by the following: 402 \begin{itemize} 403 \item 404 A data type, $M$. 405 For instance, the \texttt{option} type in O'Caml or Matita. 406 \item 407 A way to `inject' or `lift' pure values into this data type (usually called \texttt{return}). 408 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. 409 In our example, the `lifting' function for the \texttt{option} monad can be implemented as: 410 \begin{lstlisting} 411 let return x = Some x 412 \end{lstlisting} 413 \item 414 A way to `sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}. 415 Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$. 416 We can see that bind `unpacks' a monadic value, applies a function after unpacking, and `repacks' the new value in the monad. 417 In our example, the sequencing function for the \texttt{option} monad can be implemented as: 418 \begin{lstlisting} 419 let bind o f = 420 match o with 421 None > None 422 Some s > f s 423 \end{lstlisting} 424 \item 425 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. 426 These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler. 427 \end{itemize} 387 428 In the semantics of both front and backend intermediate languages, we make use of monads. 388 In particular, we make use of two forms of monad: 389 \begin{enumerate} 390 \item 391 An `error monad', which signals that a computation either has completed successfully, or returns with an error message. 392 The sequencing operation of the error monad ensures that the result of chained computations in return the error message of the first failed computation. 393 This monad is used extensively in the semantics to signal a state which cannot be recovered from. 394 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states: 395 \begin{lstlisting} 396 XXX 397 \end{lstlisting} 398 \item 399 An `IO' monad, signalling the emission or reading of data to some external location or memory address. 400 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). 429 This monadic infrastructure is shared between the frontend and backend languages. 430 431 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. 432 Here, the monad's sequencing operation ensures that emissions and reads are maintained in the correct order. 401 433 Most functions in the intermediate language semantics fall into the IO monad. 402 \end{enumerate} 403 This monadic infrastructure is shared between the frontend and backend languages. 434 In particular, we have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type: 435 \begin{lstlisting} 436 definition eval_statement: 437 ∀globals: list ident.∀p:sem_params2 globals. 438 genv globals p → state p → IO io_out io_in (trace × (state p)) := 439 ... 440 \end{lstlisting} 441 If we in the body of \texttt{eval\_statement}, we may also see how the monad sequences effects. 442 For instance, in the case for the \texttt{LOAD} statement, we have the following: 443 \begin{lstlisting} 444 definition eval_statement: 445 ∀globals: list ident. ∀p:sem_params2 globals. 446 genv globals p → state p → IO io_out io_in (trace × (state p)) := 447 $\lambda$globals, p, ge, st. 448 ... 449 match s with 450  LOAD dst addrl addrh ⇒ 451 ! vaddrh $\leftarrow$ dph_retrieve … st addrh; 452 ! vaddrl $\leftarrow$ dpl_retrieve … st addrl; 453 ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉; 454 ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr); 455 ! st $\leftarrow$ acca_store p … dst v st; 456 ! st $\leftarrow$ next … l st ; 457 ret ? $\langle$E0, st$\rangle$ 458 \end{lstlisting} 459 Here, we employ a certain degree of syntactic sugaring. 460 The syntax 461 \begin{lstlisting} 462 ... 463 ! vaddrh $\leftarrow$ dph_retrieve … st addrh; 464 ! vaddrl $\leftarrow$ dpl_retrieve … st addrl; 465 ... 466 \end{lstlisting} 467 is sugaring for the \texttt{IO} monad's binding operation. 468 We can expand this sugaring to the following much more verbose code: 469 \begin{lstlisting} 470 ... 471 bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl) 472 ($\lambda$vaddrl. ...)) 473 \end{lstlisting} 474 Note also that the function \texttt{ret} is implementing the `lifting', or return function of the \texttt{IO} monad. 475 476 We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about. 477 In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic. 478 The function \texttt{opt\_to\_res} is also  this is a `utility' function that lifts an option type into the \texttt{IO} monad. 404 479 405 480 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.