Changeset 1434
 Timestamp:
 Oct 21, 2011, 4:45:58 PM (9 years ago)
 Location:
 Deliverables/D4.24.3/reports
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.24.3/reports/D42.tex
r1432 r1434 218 218  INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals 219 219 ... 220  OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals 220  OP1: Op1 $ 221 ightarrow$ acc_a_reg p $ 222 ightarrow$ acc_a_reg p $ 223 ightarrow$ joint_instruction p globals 221 224 ... 222 225  extension: extend_statements p $\rightarrow$ joint_instruction p globals. … … 259 262 Our joint internal function record looks like so: 260 263 \begin{lstlisting} 261 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝264 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := 262 265 { 263 266 ... … … 265 268 joint_if_locals : localsT p; 266 269 ... 267 joint_if_code : codeT …p;270 joint_if_code : codeT ... p; 268 271 ... 269 272 }. … … 280 283 For instance, in the definition: 281 284 \begin{lstlisting} 282 inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝283 ... 284  INT: generic_reg p → Byte →joint_instruction p globals285  MOVE: pair_reg p →joint_instruction p globals286 ... 287  PUSH: acc_a_reg p →joint_instruction p globals288 ... 289  extension: extend_statements p →joint_instruction p globals.285 inductive joint_instruction (p:params__) (globals: list ident): Type[0] := 286 ... 287  INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals 288  MOVE: pair_reg p $\rightarrow$ joint_instruction p globals 289 ... 290  PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals 291 ... 292  extension: extend_statements p $\rightarrow$ joint_instruction p globals. 290 293 \end{lstlisting} 291 294 The capitalised constructors\texttt{INT}, \texttt{MOVE}, and so onare all machine specific instructions. … … 339 342 For instance, the \texttt{translate\_negint} function, which translates a negative integer constant: 340 343 \begin{lstlisting} 341 definition translate_negint ≝344 definition translate_negint := 342 345 $\lambda$globals: list ident. 343 346 $\lambda$destrs: list register. … … 493 496 \end{landscape} 494 497 Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question. 495 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file .498 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file(s). 496 499 These are computed with \texttt{wc l}, a standard Unix tool. 497 500 
Deliverables/D4.24.3/reports/D43.tex
r1428 r1434 177 177 This holds the types of the representations of the different register varieties in the intermediate languages: 178 178 \begin{lstlisting} 179 record params__: Type[1] ≝179 record params__: Type[1] := 180 180 { 181 181 acc_a_reg: Type[0]; … … 210 210 \begin{lstlisting} 211 211 inductive joint_instruction (p: params__) (globals: list ident): Type[0] := 212  COMMENT: String →joint_instruction p globals213  COST_LABEL: costlabel →joint_instruction p globals214 ... 215  OP1: Op1 → acc_a_reg p → acc_a_reg p →joint_instruction p globals212  COMMENT: String $\rightarrow$ joint_instruction p globals 213  COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals 214 ... 215  OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals 216 216 ... 217 217 \end{lstlisting} … … 222 222 We make a distinction between instructions that pass control onto their immediate successors, and those that jump elsewhere in the program, through the use of \texttt{succ}, denoting the immediate successor of the current instruction, in the \texttt{params\_} record described below. 223 223 \begin{lstlisting} 224 record params_: Type[1] ≝224 record params_: Type[1] := 225 225 { 226 226 pars__ :> params__; … … 232 232 \begin{lstlisting} 233 233 inductive joint_statement (p:params_) (globals: list ident): Type[0] := 234  sequential: joint_instruction p globals → succ p →joint_statement p globals235  GOTO: label →joint_statement p globals234  sequential: joint_instruction p globals $\rightarrow$ succ p $\rightarrow$ joint_statement p globals 235  GOTO: label $\rightarrow$ joint_statement p globals 236 236  RETURN: joint_statement p globals. 237 237 \end{lstlisting} … … 242 242 In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}: 243 243 \begin{lstlisting} 244 record params0: Type[1] ≝ 245 { pars__' :> params__ 246 ; resultT: Type[0] 247 ; paramsT: Type[0] 248 }. 244 record params0: Type[1] := 245 { 246 pars__' :> params__; 247 resultT: Type[0]; 248 paramsT: Type[0] 249 }. 249 250 \end{lstlisting} 250 251 Here, \texttt{resultT} and \texttt{resultT} typically are the (pseudo)registers that store the parameters and result of a function. … … 252 253 We further extend \texttt{params0} with a type for local variables in internal function calls: 253 254 \begin{lstlisting} 254 record params1 : Type[1] ≝ 255 { pars0 :> params0 256 ; localsT: Type[0] 257 }. 255 record params1 : Type[1] := 256 { 257 pars0 :> params0; 258 localsT: Type[0] 259 }. 258 260 \end{lstlisting} 259 261 Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements). … … 261 263 Note that \texttt{lookup} may fail, and returns an \texttt{option} type: 262 264 \begin{lstlisting} 263 record params (globals: list ident): Type[1] ≝ 264 { succ_ : Type[0] 265 ; pars1 :> params1 266 ; codeT: Type[0] 267 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals) 268 }. 265 record params (globals: list ident): Type[1] := 266 { 267 succ_ : Type[0]; 268 pars1 :> params1; 269 codeT : Type[0]; 270 lookup: codeT $\rightarrow$ label $\rightarrow$ option (joint_statement (mk_params_ pars1 succ_) globals) 271 }. 269 272 \end{lstlisting} 270 273 We now have what we need to define internal functions for the joint language. … … 282 285 joint_if_locals : localsT p; 283 286 joint_if_stacksize: nat; 284 joint_if_code : codeT …p;285 joint_if_entry : $\Sigma$l: label. lookup … joint_if_code l ≠None ?;286 joint_if_exit : $\Sigma$l: label. lookup … joint_if_code l ≠None ?287 joint_if_code : codeT ... p; 288 joint_if_entry : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?; 289 joint_if_exit : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ? 287 290 }. 288 291 \end{lstlisting} … … 293 296 ... 294 297 definition ertl_params__: params__ := 295 mk_params__ register register register register (move_registers ×move_registers)298 mk_params__ register register register register (move_registers $\times$ move_registers) 296 299 register nat unit ertl_statement_extension. 297 300 ... 298 301 definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0. 299 definition ertl_params: ∀globals. params globals ≝rtl_ertl_params ertl_params0.302 definition ertl_params: ∀globals. params globals := rtl_ertl_params ertl_params0. 300 303 ... 301 304 definition ertl_statement := joint_statement ertl_params_. 302 305 303 306 definition ertl_internal_function := 304 $\lambda$globals.joint_internal_function …(ertl_params globals).307 $\lambda$globals.joint_internal_function ... (ertl_params globals). 305 308 \end{lstlisting} 306 309 Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages: … … 322 325 call_dest_for_main: call_dest p; 323 326 324 succ_pc: succ p → address →res address;325 326 greg_store_: generic_reg p → beval → regsT →res regsT;327 greg_retrieve_: regsT → generic_reg p →res beval;328 acca_store_: acc_a_reg p → beval → regsT →res regsT;329 acca_retrieve_: regsT → acc_a_reg p →res beval;330 ... 331 dpl_store_: dpl_reg p → beval → regsT →res regsT;332 dpl_retrieve_: regsT → dpl_reg p →res beval;333 ... 334 pair_reg_move_: regsT → pair_reg p →res regsT;335 pointer_of_label: label →$\Sigma$p:pointer. ptype p = Code327 succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address; 328 329 greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; 330 greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval; 331 acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; 332 acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval; 333 ... 334 dpl_store_: dpl_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; 335 dpl_retrieve_: regsT $\rightarrow$ dpl_reg p $\rightarrow$ res beval; 336 ... 337 pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT; 338 pointer_of_label: label $\rightarrow$ $\Sigma$p:pointer. ptype p = Code 336 339 }. 337 340 \end{lstlisting} … … 356 359 more_sparams1 :> more_sem_params p; 357 360 fetch_statement: 358 genv … p → state (mk_sem_params … more_sparams1) →359 res (joint_statement (mk_sem_params …more_sparams1) globals);361 genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ 362 res (joint_statement (mk_sem_params ... more_sparams1) globals); 360 363 ... 361 364 save_frame: 362 address → nat → paramsT … p → call_args p → call_dest p →363 state (mk_sem_params … more_sparams1) →364 res (state (mk_sem_params …more_sparams1));365 address $\rightarrow$ nat $\rightarrow$ paramsT ... p $\rightarrow$ call_args p $\rightarrow$ call_dest p $\rightarrow$ 366 state (mk_sem_params ... more_sparams1) $\rightarrow$ 367 res (state (mk_sem_params ... more_sparams1)); 365 368 pop_frame: 366 genv globals p → state (mk_sem_params … more_sparams1) →367 res ((state (mk_sem_params …more_sparams1)));369 genv globals p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ 370 res ((state (mk_sem_params ... more_sparams1))); 368 371 ... 369 372 set_result: 370 list val → state (mk_sem_params … more_sparams1) →371 res (state (mk_sem_params …more_sparams1));373 list val $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ 374 res (state (mk_sem_params ... more_sparams1)); 372 375 exec_extended: 373 genv globals p → extend_statements (mk_sem_params … more_sparams1) →374 succ p → state (mk_sem_params … more_sparams1) →375 IO io_out io_in (trace × (state (mk_sem_params …more_sparams1)))376 genv globals p $\rightarrow$ extend_statements (mk_sem_params ... more_sparams1) $\rightarrow$ 377 succ p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ 378 IO io_out io_in (trace $\times$ (state (mk_sem_params ... more_sparams1))) 376 379 }. 377 380 \end{lstlisting} … … 414 417 definition eval_statement: 415 418 ∀globals: list ident.∀p:sem_params2 globals. 416 genv globals p → state p → IO io_out io_in (trace ×(state p)) :=419 genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) := 417 420 ... 418 421 \end{lstlisting} … … 469 472 definition eval_statement: 470 473 ∀globals: list ident.∀p:sem_params2 globals. 471 genv globals p → state p → IO io_out io_in (trace ×(state p)) :=474 genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) := 472 475 ... 473 476 \end{lstlisting} … … 477 480 definition eval_statement: 478 481 ∀globals: list ident. ∀p:sem_params2 globals. 479 genv globals p → state p → IO io_out io_in (trace ×(state p)) :=482 genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) := 480 483 $\lambda$globals, p, ge, st. 481 484 ... 482 485 match s with 483 486  LOAD dst addrl addrh ⇒ 484 ! vaddrh $\leftarrow$ dph_retrieve …st addrh;485 ! vaddrl $\leftarrow$ dpl_retrieve …st addrl;486 ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;487 ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m …st) vaddr);488 ! st $\leftarrow$ acca_store p …dst v st;489 ! st $\leftarrow$ next …l st ;487 ! vaddrh $\leftarrow$ dph_retrieve ... st addrh; 488 ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl; 489 ! vaddr $\leftarrow$ pointer_of_address $\langle$vaddrl,vaddrh$\rangle$; 490 ! v $\leftarrow$ opt_to_res ... (msg FailedLoad) (beloadv (m ... st) vaddr); 491 ! st $\leftarrow$ acca_store p ... dst v st; 492 ! st $\leftarrow$ next ... l st ; 490 493 ret ? $\langle$E0, st$\rangle$ 491 494 \end{lstlisting} … … 494 497 \begin{lstlisting} 495 498 ... 496 ! vaddrh $\leftarrow$ dph_retrieve …st addrh;497 ! vaddrl $\leftarrow$ dpl_retrieve …st addrl;499 ! vaddrh $\leftarrow$ dph_retrieve ... st addrh; 500 ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl; 498 501 ... 499 502 \end{lstlisting} … … 502 505 \begin{lstlisting} 503 506 ... 504 bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve …st addrl)507 bind (dph_retrieve ... st addrh) ($\lambda$vaddrh. bind (dpl_retrieve ... st addrl) 505 508 ($\lambda$vaddrl. ...)) 506 509 \end{lstlisting} … … 596 599 \end{table} 597 600 \end{landscape} 598 Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question.601 Here, the O'Caml column denotes the O'Caml source file(s) in the prototype compiler's implementation that corresponds to the Matita script in question. 599 602 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file. 600 603 These are computed with \texttt{wc l}, a standard Unix tool.
Note: See TracChangeset
for help on using the changeset viewer.