Changeset 1434 for Deliverables/D4.2-4.3


Ignore:
Timestamp:
Oct 21, 2011, 4:45:58 PM (8 years ago)
Author:
mulligan
Message:

chages to typesetting and some wording changes

Location:
Deliverables/D4.2-4.3/reports
Files:
2 edited

Legend:

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

    r1432 r1434  
    218218  | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals
    219219  ...
    220   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     220  | OP1: Op1 $
     221ightarrow$ acc_a_reg p $
     222ightarrow$ acc_a_reg p $
     223ightarrow$ joint_instruction p globals
    221224  ...
    222225  | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
     
    259262Our joint internal function record looks like so:
    260263\begin{lstlisting}
    261 record joint_internal_function (globals: list ident) (p:params globals) : Type[0]
     264record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
    262265{
    263266  ...
     
    265268  joint_if_locals   : localsT p;
    266269  ...
    267   joint_if_code     : codeT p;
     270  joint_if_code     : codeT ... p;
    268271  ...
    269272}.
     
    280283For instance, in the definition:
    281284\begin{lstlisting}
    282 inductive joint_instruction (p:params__) (globals: list ident): Type[0]
    283   ...
    284   | INT: generic_reg p → Byte → joint_instruction p globals
    285   | MOVE: pair_reg p joint_instruction p globals
    286   ...
    287   | PUSH: acc_a_reg p joint_instruction p globals
    288   ...
    289   | extension: extend_statements p joint_instruction p globals.
     285inductive joint_instruction (p:params__) (globals: list ident): Type[0] :=
     286  ...
     287  | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals
     288  | MOVE: pair_reg p $\rightarrow$ joint_instruction p globals
     289  ...
     290  | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals
     291  ...
     292  | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
    290293\end{lstlisting}
    291294The capitalised constructors---\texttt{INT}, \texttt{MOVE}, and so on---are all machine specific instructions.
     
    339342For instance, the \texttt{translate\_negint} function, which translates a negative integer constant:
    340343\begin{lstlisting}
    341 definition translate_negint
     344definition translate_negint :=
    342345  $\lambda$globals: list ident.
    343346  $\lambda$destrs: list register.
     
    493496\end{landscape}
    494497Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question.
    495 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
     498The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file(s).
    496499These are computed with \texttt{wc -l}, a standard Unix tool.
    497500
  • Deliverables/D4.2-4.3/reports/D4-3.tex

    r1428 r1434  
    177177This holds the types of the representations of the different register varieties in the intermediate languages:
    178178\begin{lstlisting}
    179 record params__: Type[1]
     179record params__: Type[1] :=
    180180{
    181181  acc_a_reg: Type[0];
     
    210210\begin{lstlisting}
    211211inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
    212   | COMMENT: String joint_instruction p globals
    213   | COST_LABEL: costlabel joint_instruction p globals
    214   ...
    215   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     212  | COMMENT: String $\rightarrow$ joint_instruction p globals
     213  | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
     214  ...
     215  | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals
    216216  ...
    217217\end{lstlisting}
     
    222222We make a distinction between instructions that pass control onto their immediate successors, and those that jump elsewhere in the program, through the use of \texttt{succ}, denoting the immediate successor of the current instruction, in the \texttt{params\_} record described below.
    223223\begin{lstlisting}
    224 record params_: Type[1]
     224record params_: Type[1] :=
    225225{
    226226  pars__ :> params__;
     
    232232\begin{lstlisting}
    233233inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
    234   | sequential: joint_instruction p globals → succ p → joint_statement p globals
    235   | GOTO: label joint_statement p globals
     234  | sequential: joint_instruction p globals $\rightarrow$ succ p $\rightarrow$ joint_statement p globals
     235  | GOTO: label $\rightarrow$ joint_statement p globals
    236236  | RETURN: joint_statement p globals.
    237237\end{lstlisting}
     
    242242In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
    243243\begin{lstlisting}
    244 record params0: Type[1] ≝
    245  { pars__' :> params__
    246  ; resultT: Type[0]
    247  ; paramsT: Type[0]
    248  }.
     244record params0: Type[1] :=
     245{
     246  pars__' :> params__;
     247  resultT: Type[0];
     248  paramsT: Type[0]
     249}.
    249250\end{lstlisting}
    250251Here, \texttt{resultT} and \texttt{resultT} typically are the (pseudo)registers that store the parameters and result of a function.
     
    252253We further extend \texttt{params0} with a type for local variables in internal function calls:
    253254\begin{lstlisting}
    254 record params1 : Type[1] ≝
    255  { pars0 :> params0
    256  ; localsT: Type[0]
    257  }.
     255record params1 : Type[1] :=
     256{
     257  pars0 :> params0;
     258  localsT: Type[0]
     259}.
    258260\end{lstlisting}
    259261Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
     
    261263Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
    262264\begin{lstlisting}
    263 record params (globals: list ident): Type[1] ≝
    264  { succ_ : Type[0]
    265  ; pars1 :> params1
    266  ; codeT: Type[0]
    267  ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
    268  }.
     265record params (globals: list ident): Type[1] :=
     266{
     267  succ_ : Type[0];
     268  pars1 :> params1;
     269  codeT : Type[0];
     270  lookup: codeT $\rightarrow$ label $\rightarrow$ option (joint_statement (mk_params_ pars1 succ_) globals)
     271}.
    269272\end{lstlisting}
    270273We now have what we need to define internal functions for the joint language.
     
    282285  joint_if_locals   : localsT p;
    283286  joint_if_stacksize: nat;
    284   joint_if_code     : codeT p;
    285   joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
    286   joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
     287  joint_if_code     : codeT ... p;
     288  joint_if_entry    : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?;
     289  joint_if_exit     : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?
    287290}.
    288291\end{lstlisting}
     
    293296...
    294297definition ertl_params__: params__ :=
    295  mk_params__ register register register register (move_registers × move_registers)
     298 mk_params__ register register register register (move_registers $\times$ move_registers)
    296299  register nat unit ertl_statement_extension.
    297300...
    298301definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0.
    299 definition ertl_params: ∀globals. params globals rtl_ertl_params ertl_params0.
     302definition ertl_params: ∀globals. params globals := rtl_ertl_params ertl_params0.
    300303...
    301304definition ertl_statement := joint_statement ertl_params_.
    302305
    303306definition ertl_internal_function :=
    304   $\lambda$globals.joint_internal_function (ertl_params globals).
     307  $\lambda$globals.joint_internal_function ... (ertl_params globals).
    305308\end{lstlisting}
    306309Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages:
     
    322325  call_dest_for_main: call_dest p;
    323326
    324   succ_pc: succ p → address → res address;
    325 
    326   greg_store_: generic_reg p → beval → regsT → res regsT;
    327   greg_retrieve_: regsT → generic_reg p → res beval;
    328   acca_store_: acc_a_reg p → beval → regsT → res regsT;
    329   acca_retrieve_: regsT → acc_a_reg p → res beval;
    330   ...
    331   dpl_store_: dpl_reg p → beval → regsT → res regsT;
    332   dpl_retrieve_: regsT → dpl_reg p → res beval;
    333   ...
    334   pair_reg_move_: regsT → pair_reg p → res regsT;
    335   pointer_of_label: label $\Sigma$p:pointer. ptype p = Code
     327  succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address;
     328
     329  greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
     330  greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval;
     331  acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
     332  acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval;
     333  ...
     334  dpl_store_: dpl_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
     335  dpl_retrieve_: regsT $\rightarrow$ dpl_reg p $\rightarrow$ res beval;
     336  ...
     337  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT;
     338  pointer_of_label: label $\rightarrow$ $\Sigma$p:pointer. ptype p = Code
    336339}.
    337340\end{lstlisting}
     
    356359  more_sparams1 :> more_sem_params p;
    357360  fetch_statement:
    358     genv … p → state (mk_sem_params … more_sparams1) →
    359     res (joint_statement (mk_sem_params more_sparams1) globals);
     361    genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
     362    res (joint_statement (mk_sem_params ... more_sparams1) globals);
    360363  ...
    361364  save_frame:
    362     address → nat → paramsT … p → call_args p → call_dest p →
    363     state (mk_sem_params … more_sparams1) →
    364     res (state (mk_sem_params more_sparams1));
     365    address $\rightarrow$ nat $\rightarrow$ paramsT ... p $\rightarrow$ call_args p $\rightarrow$ call_dest p $\rightarrow$
     366    state (mk_sem_params ... more_sparams1) $\rightarrow$
     367    res (state (mk_sem_params ... more_sparams1));
    365368  pop_frame:
    366     genv globals p → state (mk_sem_params … more_sparams1) →
    367     res ((state (mk_sem_params more_sparams1)));
     369    genv globals p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
     370    res ((state (mk_sem_params ... more_sparams1)));
    368371  ...
    369372  set_result:
    370     list val → state (mk_sem_params … more_sparams1) →
    371     res (state (mk_sem_params more_sparams1));
     373    list val $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
     374    res (state (mk_sem_params ... more_sparams1));
    372375  exec_extended:
    373     genv globals p → extend_statements (mk_sem_params … more_sparams1) →
    374     succ p → state (mk_sem_params … more_sparams1) →
    375     IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
     376    genv globals p $\rightarrow$ extend_statements (mk_sem_params ... more_sparams1) $\rightarrow$
     377    succ p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
     378    IO io_out io_in (trace $\times$ (state (mk_sem_params ... more_sparams1)))
    376379 }.
    377380\end{lstlisting}
     
    414417definition eval_statement:
    415418  ∀globals: list ident.∀p:sem_params2 globals.
    416     genv globals p → state p → IO io_out io_in (trace × (state p)) :=
     419    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
    417420...
    418421\end{lstlisting}
     
    469472definition eval_statement:
    470473  ∀globals: list ident.∀p:sem_params2 globals.
    471     genv globals p → state p → IO io_out io_in (trace × (state p)) :=
     474    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
    472475...
    473476\end{lstlisting}
     
    477480definition eval_statement:
    478481  ∀globals: list ident. ∀p:sem_params2 globals.
    479     genv globals p → state p → IO io_out io_in (trace × (state p)) :=
     482    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
    480483  $\lambda$globals, p, ge, st.
    481484  ...
    482485  match s with
    483486  | LOAD dst addrl addrh ⇒
    484     ! vaddrh $\leftarrow$ dph_retrieve st addrh;
    485     ! vaddrl $\leftarrow$ dpl_retrieve st addrl;
    486     ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;
    487     ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    488     ! st $\leftarrow$ acca_store p dst v st;
    489     ! st $\leftarrow$ next l st ;
     487    ! vaddrh $\leftarrow$ dph_retrieve ... st addrh;
     488    ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl;
     489    ! vaddr $\leftarrow$ pointer_of_address $\langle$vaddrl,vaddrh$\rangle$;
     490    ! v $\leftarrow$ opt_to_res ... (msg FailedLoad) (beloadv (m ... st) vaddr);
     491    ! st $\leftarrow$ acca_store p ... dst v st;
     492    ! st $\leftarrow$ next ... l st ;
    490493      ret ? $\langle$E0, st$\rangle$
    491494\end{lstlisting}
     
    494497\begin{lstlisting}
    495498  ...
    496 ! vaddrh $\leftarrow$ dph_retrieve st addrh;
    497 ! vaddrl $\leftarrow$ dpl_retrieve st addrl;
     499! vaddrh $\leftarrow$ dph_retrieve ... st addrh;
     500! vaddrl $\leftarrow$ dpl_retrieve ... st addrl;
    498501  ...
    499502\end{lstlisting}
     
    502505\begin{lstlisting}
    503506  ...
    504   bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl)
     507  bind (dph_retrieve ... st addrh) ($\lambda$vaddrh. bind (dpl_retrieve ... st addrl)
    505508    ($\lambda$vaddrl. ...))
    506509\end{lstlisting}
     
    596599\end{table}
    597600\end{landscape}
    598 Here, the O'Caml column denotes the O'Caml source file in the prototype compiler's implementation that corresponds to the Matita script in question.
     601Here, the O'Caml column denotes the O'Caml source file(s) in the prototype compiler's implementation that corresponds to the Matita script in question.
    599602The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
    600603These are computed with \texttt{wc -l}, a standard Unix tool.
Note: See TracChangeset for help on using the changeset viewer.