# Changeset 1399 for Deliverables/D4.2-4.3/reports

Ignore:
Timestamp:
Oct 18, 2011, 11:38:37 AM (9 years ago)
Message:

more work on parameters

File:
1 edited

### Legend:

Unmodified
 r1398 \lstdefinelanguage{matita-ocaml} {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try}, morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct}, {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,let,in,rec,match,return,with,Type,try}, morekeywords={[2]whd,normalize,elim,cases,destruct}, morekeywords={[3]type,of}, mathescape=true, }. \end{lstlisting} Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements). Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}. Note that \texttt{lookup} may fail, and returns an \texttt{option} type: \begin{lstlisting} record params (globals: list ident): Type[1] ≝ }. \end{lstlisting} \begin{lstlisting} definition graph_params_: params__ $\rightarrow$ params_ := $\lambda$pars__. mk_params_ pars__ label. \end{lstlisting} We now have what we need to define internal functions for the joint language. The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics. The rest of the fields affect both compilation and semantics. In particular, we have parameterised result types, function parameter types and the type of local variables. 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: \begin{lstlisting} record joint_internal_function (globals: list ident) (p:params globals) : Type[0] := joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ? }. \end{lstlisting} 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. The reason is because some intermediate languages share a host of parameters, and only differ on some others. For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific: \begin{lstlisting} ... definition ertl_params__: params__ := mk_params__ register register register register (move_registers × move_registers) register nat unit ertl_statement_extension. ... definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0. definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0. ... definition ertl_statement := joint_statement ertl_params_. definition ertl_internal_function := $\lambda$globals.joint_internal_function … (ertl_params globals). \end{lstlisting} Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages: \begin{lstlisting} definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register). \end{lstlisting}