Changeset 1397


Ignore:
Timestamp:
Oct 17, 2011, 6:37:58 PM (8 years ago)
Author:
mulligan
Message:

more changes, talking about parameters

File:
1 edited

Legend:

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

    r1394 r1397  
    162162% SECTION.                                                                    %
    163163%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     164\subsection{Type parameters, and their purpose}
     165\label{subsect.type.parameters.their.purpose}
     166
     167We mentioned in the Deliverable D4.2 report that all joint languages are parameterised by a number of types, which are later specialised to each distinct intermediate language.
     168As this parameterisation process is also dependent on designs decisions in the language semantics, we have so far held off summarising the role of each parameter.
     169We now summarise what each parameter is.
     170
     171\begin{lstlisting}
     172record params__: Type[1] ≝
     173{
     174  acc_a_reg: Type[0];
     175  acc_b_reg: Type[0];
     176  dpl_reg: Type[0];
     177  dph_reg: Type[0];
     178  pair_reg: Type[0];
     179  generic_reg: Type[0];
     180  call_args: Type[0];
     181  call_dest: Type[0];
     182  extend_statements: Type[0]
     183}.
     184\end{lstlisting}
     185
     186As 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:
     187\begin{lstlisting}
     188inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
     189  | COMMENT: String → joint_instruction p globals
     190  | COST_LABEL: costlabel → joint_instruction p globals
     191  ...
     192\end{lstlisting}
     193
     194We extend \texttt{params\_\_} with a type corresponding
     195\begin{lstlisting}
     196record params_: Type[1] ≝
     197{
     198  pars__ :> params__;
     199  succ: Type[0]
     200}.
     201\end{lstlisting}
     202
     203\begin{lstlisting}
     204inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
     205  | sequential: joint_instruction p globals → succ p → joint_statement p globals
     206  | GOTO: label → joint_statement p globals
     207  | RETURN: joint_statement p globals.
     208\end{lstlisting}
     209
     210\begin{lstlisting}
     211record params0: Type[1] ≝
     212 { pars__' :> params__
     213 ; resultT: Type[0]
     214 ; paramsT: Type[0]
     215 }.
     216\end{lstlisting}
     217
     218\begin{lstlisting}
     219record params1 : Type[1] ≝
     220 { pars0 :> params0
     221 ; localsT: Type[0]
     222 }.
     223\end{lstlisting}
     224
     225\begin{lstlisting}
     226record params (globals: list ident): Type[1] ≝
     227 { succ_ : Type[0]
     228 ; pars1 :> params1
     229 ; codeT: Type[0]
     230 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
     231 }.
     232\end{lstlisting}
     233
     234\begin{lstlisting}
     235definition graph_params_: params__ $\rightarrow$ params_ :=
     236  $\lambda$pars__. mk_params_ pars__ label.
     237\end{lstlisting}
     238
     239\begin{lstlisting}
     240record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
     241{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
     242  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     243(*  joint_if_sig: signature;  -- dropped in front end *)
     244  joint_if_result   : resultT p;
     245  joint_if_params   : paramsT p;
     246  joint_if_locals   : localsT p;
     247(*CSC: XXXXX stacksize unused for LTL-...*)
     248  joint_if_stacksize: nat;
     249  joint_if_code     : codeT … p;
     250(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
     251  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
     252(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
     253  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
     254}.
     255\end{lstlisting}
     256
     257%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     258% SECTION.                                                                    %
     259%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    164260\subsection{Use of monads}
    165261\label{subsect.use.of.monads}
     
    178274For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
    179275\begin{lstlisting}
    180 ...
    181 | Returnstate v dst fs m $\Rightarrow$
    182   match fs with
    183   [ nil ⇒ Error $\ldots$ (msg FinalState) (* Already in final state *)
    184   | cons f fs' $\Rightarrow$
    185     ! locals $\leftarrow$ match dst with
    186     [ None $\Rightarrow$
    187       match v with
    188       [ None $\Rightarrow$ OK $\ldots$ (locals f)
    189       | _ $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch)
    190       ]
    191     | Some d $\Rightarrow$
    192       match v with
    193       [ None $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch)
    194       | Some v' $\Rightarrow$ reg_store d v' (locals f)
    195       ]
    196     ];
    197     ret $\ldots$ $\langle$E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m$\rangle$
    198   ]
    199 ...
     276XXX better example
    200277\end{lstlisting}
    201278\item
Note: See TracChangeset for help on using the changeset viewer.