Changeset 1361


Ignore:
Timestamp:
Oct 12, 2011, 11:52:23 AM (8 years ago)
Author:
mulligan
Message:

more changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1360 r1361  
    139139% SECTION.                                                                    %
    140140%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    141 \subsection{A brief overview of the compilation chain}
    142 \label{subsect.brief.overview.compilation.chain}
    143 
    144 
     141\subsection{A brief overview of the backend compilation chain}
     142\label{subsect.brief.overview.backend.compilation.chain}
     143
     144The compiler's backend consists of four distinct intermediate languages: RTL, ERTL, LTL and LIN.
     145A fifth language, RTLabs, serves as the exit point of the backend and the entry point of the frontend.
     146RTL, ERTL and LTL are `graph based' languages, whereas LIN is a linearised language
     147
     148\paragraph{RTL (Register Transfer Language)}
     149
     150\paragraph{ERTL (Extended Register Transfer Language)}
     151
     152\paragraph{LTL (Linearised Transfer Language)}
     153
     154\paragraph{LIN (Linearised)}
    145155
    146156%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    169179We now discuss some abstractions, introduced in the Matita code, which we hope will make our proofs shorter, amongst other benefits.
    170180
    171 \paragraph{Shared code}
     181\paragraph{Shared code, reduced proofs}
    172182Many features of individual backend intermediate languages are shared with other intermediate languages.
    173183For instance, RTLabs, RTL, ERTL and LTL are all graph based languages, where functions are represented as a graph of statements that form their bodies.
    174184Functions for adding statements to a graph, searching the graph, and so on, are remarkably similar across all languages, but are duplicated in the O'Caml code.
     185
     186\paragraph{Changes between languages made explicit}
     187
     188\paragraph{Possible language commutations}
     189
     190\paragraph{Instruction selection}
    175191
    176192%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.