Changeset 1399 for Deliverables/D4.2-4.3/reports/D4-3.tex
- Timestamp:
- Oct 18, 2011, 11:38:37 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1398 r1399 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,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, … … 247 247 }. 248 248 \end{lstlisting} 249 249 Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements). 250 Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}. 251 Note that \texttt{lookup} may fail, and returns an \texttt{option} type: 250 252 \begin{lstlisting} 251 253 record params (globals: list ident): Type[1] ≝ … … 256 258 }. 257 259 \end{lstlisting} 258 259 \begin{lstlisting} 260 definition graph_params_: params__ $\rightarrow$ params_ := 261 $\lambda$pars__. mk_params_ pars__ label. 262 \end{lstlisting} 263 260 We now have what we need to define internal functions for the joint language. 261 The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics. 262 The rest of the fields affect both compilation and semantics. 263 In particular, we have parameterised result types, function parameter types and the type of local variables. 264 Note also that we have lifted the hypothesised \texttt{lookup} function from \texttt{params} into a dependent sigma type, which combines a label (the entry and exit points of the control flow graph or list) combined with a proof that the label is in the graph structure: 264 265 \begin{lstlisting} 265 266 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := … … 278 279 joint_if_exit : $\Sigma$l: label. lookup … joint_if_code l ≠ None ? 279 280 }. 281 \end{lstlisting} 282 Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones. 283 The reason is because some intermediate languages share a host of parameters, and only differ on some others. 284 For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific: 285 \begin{lstlisting} 286 ... 287 definition ertl_params__: params__ := 288 mk_params__ register register register register (move_registers × move_registers) 289 register nat unit ertl_statement_extension. 290 ... 291 definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0. 292 definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0. 293 ... 294 definition ertl_statement := joint_statement ertl_params_. 295 296 definition ertl_internal_function := 297 $\lambda$globals.joint_internal_function … (ertl_params globals). 298 \end{lstlisting} 299 Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages: 300 \begin{lstlisting} 301 definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register). 280 302 \end{lstlisting} 281 303
Note: See TracChangeset
for help on using the changeset viewer.