Changeset 1364 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 13, 2011, 11:11:03 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1362 r1364 20 20 21 21 \lstdefinelanguage{matita-ocaml} 22 {keywords={ ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},23 morekeywords={[2] nwhd,nnormalize,nelim,ncases,ndestruct},22 {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try}, 23 morekeywords={[2]whd,normalize,elim,cases,destruct}, 24 24 morekeywords={[3]type,of}, 25 25 mathescape=true, … … 289 289 $\lambda$dest_lbl: label. 290 290 $\lambda$def: rtl_internal_function globals. 291 $\lambda$prf: |destrs| = |srcrs|. (* assert in caml code *)291 $\lambda$prf: |destrs| = |srcrs|. (* assert here *) 292 292 ... 293 293 \end{lstlisting} … … 424 424 % SECTION. % 425 425 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% 426 \subsection{Listing of important functions} 427 \label{subsect.listing.important.functions} 426 \subsection{Listing of important functions and axioms} 427 \label{subsect.listing.important.functions.and.axioms} 428 429 We list some important functions in the backend compilation: 430 431 \paragraph{From RTL/RTLabsToRTL.ma} 432 \begin{center} 433 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 434 Title & Description \\ 435 \hline 436 \texttt{translate\_stmt} & Translation of an RTLabs statement to an RTL statement \\ 437 \texttt{translate\_internal} & Translation of an RTLabs internal function to an RTL internal function \\ 438 \texttt{rtlabs\_to\_rtl} & Translation of an RTLabs program to an RTL program 439 \end{tabular*} 440 \end{center} 441 442 \paragraph{From joint/TranslateUtils.ma} 443 \begin{center} 444 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 445 Title & Description \\ 446 \hline 447 \texttt{fresh\_regs} & Generic fresh pseudoregister generation, for any intermediate language \\ 448 \texttt{adds\_graph} & Generic means of adding a statement to a graph, for any intermediate language 449 \end{tabular*} 450 \end{center} 451 452 \paragraph{From RTL/RTLTailcall.ma} 453 \begin{center} 454 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 455 Title & Description \\ 456 \hline 457 \texttt{simplify\_statement} & Remove a single tailcall \\ 458 \texttt{simplify\_graph} & Remove all tailcalls in the function graph \\ 459 \texttt{tailcall\_simplify} & Simplify an RTL program by removing tailcalls 460 \end{tabular*} 461 \end{center} 462 463 \paragraph{From RTL/RTLToERTL.ma} 464 \begin{center} 465 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 466 Title & Description \\ 467 \hline 468 \texttt{translate\_stmt} & Translation of an RTL statement to an ERTL statement \\ 469 \texttt{translate\_funct\_internal} & Translation of an RTL internal function to an ERTL internal function \\ 470 \texttt{translate} & Translation of an RTL program to an ERTL program 471 \end{tabular*} 472 \end{center} 473 474 \paragraph{From ERTL/liveness.ma} 475 \begin{center} 476 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 477 Title & Description \\ 478 \hline 479 \texttt{analyse} & Dead code analysis 480 \end{tabular*} 481 \end{center} 482 483 \paragraph{From ERTL/Interference.ma} 484 \begin{center} 485 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 486 Title & Description \\ 487 \hline 488 \texttt{build} & The (axiomatised) graph colouring for register and stack slot allocation 489 \end{tabular*} 490 \end{center} 491 492 \paragraph{From ERTL/ERTLToLTL.ma} 493 \begin{center} 494 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 495 Title & Description \\ 496 \hline 497 \texttt{translate\_statement} & Translation of an ERTL statement into multiple LTL statements \\ 498 \texttt{translate\_internal} & Translation of an ERTL internal function into an LTL internal function \\ 499 \texttt{ertl\_to\_ltl} & Translation of an ERTL program into an LTL program 500 \end{tabular*} 501 \end{center} 502 503 \paragraph{From LTL/LTLToLIN.ma} 504 \begin{center} 505 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 506 Title & Description \\ 507 \hline 508 \texttt{visit} & Visits, in order, every node in the statement graph for linearisation \\ 509 \texttt{translate\_stmt} & Translation of an LTL statement to a LIN statement \\ 510 \texttt{branch\_compress} & Place holder (currently identity) function for branch compression \\ 511 \texttt{translate\_internal} & Translation of an LTL internal function into a LIN internal function \\ 512 \texttt{ltl\_to\_lin} & Translation of an LTL program to a LIN program 513 \end{tabular*} 514 \end{center} 515 516 \paragraph{From LIN/LINToASM.ma} 517 \begin{center} 518 \begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}} 519 Title & Description \\ 520 \hline 521 \texttt{translate\_statements} & Translation of a LIN statement to mutliple assembly instructions \\ 522 \texttt{translate\_fun\_def} & Translation of a LIN internal function definition into assembly \\ 523 \texttt{translate} & Translation of a LIN program into assembly 524 \end{tabular*} 525 \end{center} 428 526 429 527 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.