Changeset 1403 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 18, 2011, 3:12:48 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1402 r1403 266 266 \begin{lstlisting} 267 267 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := 268 { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*)269 joint_if_ runiverse: universe RegisterTag; (*CSC: used only for compilation*)270 (* joint_if_sig: signature; -- dropped in front end *) 268 { 269 joint_if_luniverse: universe LabelTag; 270 joint_if_runiverse: universe RegisterTag; 271 271 joint_if_result : resultT p; 272 272 joint_if_params : paramsT p; 273 273 joint_if_locals : localsT p; 274 (*CSC: XXXXX stacksize unused for LTL-...*)275 274 joint_if_stacksize: nat; 276 275 joint_if_code : codeT … p; 277 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)278 276 joint_if_entry : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?; 279 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)280 277 joint_if_exit : $\Sigma$l: label. lookup … joint_if_code l ≠ None ? 281 278 }. … … 303 300 \end{lstlisting} 304 301 302 \begin{lstlisting} 303 record more_sem_params (p:params_): Type[1] := 304 { 305 framesT: Type[0]; 306 regsT: Type[0]; 307 succ_pc: succ p → address → res address; 308 greg_store_: generic_reg p → beval → regsT → res regsT; 309 greg_retrieve_: regsT → generic_reg p → res beval; 310 acca_store_: acc_a_reg p → beval → regsT → res regsT; 311 acca_retrieve_: regsT → acc_a_reg p → res beval; 312 accb_store_: acc_b_reg p → beval → regsT → res regsT; 313 accb_retrieve_: regsT → acc_b_reg p → res beval; 314 dpl_store_: dpl_reg p → beval → regsT → res regsT; 315 dpl_retrieve_: regsT → dpl_reg p → res beval; 316 dph_store_: dph_reg p → beval → regsT → res regsT; 317 dph_retrieve_: regsT → dph_reg p → res beval; 318 pair_reg_move_: regsT → pair_reg p → res regsT; 319 pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code 320 }. 321 \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 331 \begin{lstlisting} 332 record state (p: sem_params): Type[0] := 333 { 334 st_frms: framesT ? p; 335 pc: address; 336 sp: pointer; 337 carry: beval; 338 regs: regsT ? p; 339 m: bemem 340 }. 341 \end{lstlisting} 342 343 \begin{lstlisting} 344 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] := 345 { 346 more_sparams1 :> more_sem_params p; 347 fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals); 348 fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address); 349 result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p)); 350 init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1; 351 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)); 352 pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1))); 353 fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val); 354 set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)); 355 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))) 356 }. 357 \end{lstlisting} 358 359 \begin{lstlisting} 360 record sem_params2 (globals: list ident): Type[1] := 361 { 362 p2 :> params globals; 363 more_sparams2 :> more_sem_params2 globals p2 364 }. 365 \end{lstlisting} 366 305 367 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 306 368 % SECTION. % … … 322 384 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states: 323 385 \begin{lstlisting} 386 XXX 324 387 \end{lstlisting} 325 388 \item
Note: See TracChangeset
for help on using the changeset viewer.