Changeset 1398


Ignore:
Timestamp:
Oct 17, 2011, 8:20:05 PM (8 years ago)
Author:
mulligan
Message:

more work on parameters

File:
1 edited

Legend:

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

    r1397 r1398  
    9797\vspace*{7cm}
    9898\paragraph{Abstract}
     99We describe the encoding in the Calculus of Constructions of the semantics of the CerCo compiler's backend intermediate languages.
     100The CerCo backend consists of five distinct languages: RTL, RTLntl, ERTL, LTL and LIN.
     101We describe a process of heavy abstraction of the intermediate languages and their semantics.
     102We hope that this process will ease the burden of Deliverable D4.4, the proof of correctness for the compiler.
    99103
    100104\newpage
     
    183187}.
    184188\end{lstlisting}
     189We summarise what these types mean:
     190\begin{center}
     191\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
     192Type & Explanation \\
     193\hline
     194\texttt{acc\_a\_reg} & The type of the accumulator A register.  In some languages this is implemented as the hardware accumulator, whereas in others this is a pseudoregister.\\
     195\texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\
     196\texttt{dpl\_reg} & \\
     197\texttt{dph\_reg} & \\
     198\texttt{pair\_reg} & \\
     199\texttt{generic\_reg} & \\
     200\texttt{call\_args} & \\
     201\texttt{call\_dest} & \\
     202\texttt{extend\_statements} &
     203\end{tabular*}
     204\end{center}
    185205
    186206As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages:
     
    192212\end{lstlisting}
    193213
    194 We extend \texttt{params\_\_} with a type corresponding
     214We extend \texttt{params\_\_} with a type corresponding to labels, \texttt{succ}, obtaining a new record type of parameters called \texttt{params\_}:
    195215\begin{lstlisting}
    196216record params_: Type[1] ≝
     
    200220}.
    201221\end{lstlisting}
    202 
     222The type \texttt{succ} corresponds to labels, in the case of control flow graph based languages, or is instantiated to the unit type for the linearised language, LIN.
     223Using \texttt{param\_} we can define statements of the joint language:
    203224\begin{lstlisting}
    204225inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
     
    207228  | RETURN: joint_statement p globals.
    208229\end{lstlisting}
    209 
     230Note that in the joint language, instructions are `linear', in that they have an immediate successor.
     231Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program.
     232
     233For the semantics, we need further parametererised types.
     234In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
    210235\begin{lstlisting}
    211236record params0: Type[1] ≝
     
    215240 }.
    216241\end{lstlisting}
    217 
     242We further extend \texttt{params0} with a type for local variables in internal function calls:
    218243\begin{lstlisting}
    219244record params1 : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.