Changeset 1399


Ignore:
Timestamp:
Oct 18, 2011, 11:38:37 AM (9 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

    r1398 r1399  
    2020
    2121\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},
    2424   morekeywords={[3]type,of},
    2525   mathescape=true,
     
    247247 }.
    248248\end{lstlisting}
    249 
     249Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
     250Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}.
     251Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
    250252\begin{lstlisting}
    251253record params (globals: list ident): Type[1] ≝
     
    256258 }.
    257259\end{lstlisting}
    258 
    259 \begin{lstlisting}
    260 definition graph_params_: params__ $\rightarrow$ params_ :=
    261   $\lambda$pars__. mk_params_ pars__ label.
    262 \end{lstlisting}
    263 
     260We now have what we need to define internal functions for the joint language.
     261The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics.
     262The rest of the fields affect both compilation and semantics.
     263In particular, we have parameterised result types, function parameter types and the type of local variables.
     264Note 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:
    264265\begin{lstlisting}
    265266record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
     
    278279  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
    279280}.
     281\end{lstlisting}
     282Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones.
     283The reason is because some intermediate languages share a host of parameters, and only differ on some others.
     284For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific:
     285\begin{lstlisting}
     286...
     287definition ertl_params__: params__ :=
     288 mk_params__ register register register register (move_registers × move_registers)
     289  register nat unit ertl_statement_extension.
     290...
     291definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0.
     292definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
     293...
     294definition ertl_statement := joint_statement ertl_params_.
     295
     296definition ertl_internal_function :=
     297  $\lambda$globals.joint_internal_function … (ertl_params globals).
     298\end{lstlisting}
     299Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages:
     300\begin{lstlisting}
     301definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register).
    280302\end{lstlisting}
    281303
Note: See TracChangeset for help on using the changeset viewer.