Changeset 1397 for Deliverables/D4.24.3
 Timestamp:
 Oct 17, 2011, 6:37:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.24.3/reports/D43.tex
r1394 r1397 162 162 % SECTION. % 163 163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 164 \subsection{Type parameters, and their purpose} 165 \label{subsect.type.parameters.their.purpose} 166 167 We 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. 168 As 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. 169 We now summarise what each parameter is. 170 171 \begin{lstlisting} 172 record 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 186 As 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} 188 inductive 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 194 We extend \texttt{params\_\_} with a type corresponding 195 \begin{lstlisting} 196 record params_: Type[1] ≝ 197 { 198 pars__ :> params__; 199 succ: Type[0] 200 }. 201 \end{lstlisting} 202 203 \begin{lstlisting} 204 inductive 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} 211 record params0: Type[1] ≝ 212 { pars__' :> params__ 213 ; resultT: Type[0] 214 ; paramsT: Type[0] 215 }. 216 \end{lstlisting} 217 218 \begin{lstlisting} 219 record params1 : Type[1] ≝ 220 { pars0 :> params0 221 ; localsT: Type[0] 222 }. 223 \end{lstlisting} 224 225 \begin{lstlisting} 226 record 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} 235 definition graph_params_: params__ $\rightarrow$ params_ := 236 $\lambda$pars__. mk_params_ pars__ label. 237 \end{lstlisting} 238 239 \begin{lstlisting} 240 record 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 164 260 \subsection{Use of monads} 165 261 \label{subsect.use.of.monads} … … 178 274 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states: 179 275 \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 ... 276 XXX better example 200 277 \end{lstlisting} 201 278 \item
Note: See TracChangeset
for help on using the changeset viewer.