Changeset 1434 for Deliverables/D4.2-4.3/reports/D4-3.tex

Timestamp:

Oct 21, 2011, 4:45:58 PM (9 years ago)

Author:

mulligan

Message:

chages to typesetting and some wording changes

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (17 diffs)

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -177 +177 @@
 This holds the types of the representations of the different register varieties in the intermediate languages:
 \begin{lstlisting}
-record params__: Type[1] ≝
+record params__: Type[1] :=
 {
   acc_a_reg: Type[0];
@@ -210 +210 @@
 \begin{lstlisting}
 inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
-  | COMMENT: String → joint_instruction p globals
-  | COST_LABEL: costlabel → joint_instruction p globals
-  ...
-  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
+  | COMMENT: String $\rightarrow$ joint_instruction p globals
+  | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
+  ...
+  | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals
   ...
 \end{lstlisting}
@@ -222 +222 @@
 We 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.
 \begin{lstlisting}
-record params_: Type[1] ≝
+record params_: Type[1] :=
 {
   pars__ :> params__;
@@ -232 +232 @@
 \begin{lstlisting}
 inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
-  | sequential: joint_instruction p globals → succ p → joint_statement p globals
-  | GOTO: label → joint_statement p globals
+  | sequential: joint_instruction p globals $\rightarrow$ succ p $\rightarrow$ joint_statement p globals
+  | GOTO: label $\rightarrow$ joint_statement p globals
   | RETURN: joint_statement p globals.
 \end{lstlisting}
@@ -242 +242 @@
 In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
 \begin{lstlisting}
-record params0: Type[1] ≝
- { pars__' :> params__
- ; resultT: Type[0]
- ; paramsT: Type[0]
- }.
+record params0: Type[1] :=
+{
+  pars__' :> params__;
+  resultT: Type[0];
+  paramsT: Type[0]
+}.
 \end{lstlisting}
 Here, \texttt{resultT} and \texttt{resultT} typically are the (pseudo)registers that store the parameters and result of a function.
@@ -252 +253 @@
 We further extend \texttt{params0} with a type for local variables in internal function calls:
 \begin{lstlisting}
-record params1 : Type[1] ≝
- { pars0 :> params0
- ; localsT: Type[0]
- }.
+record params1 : Type[1] :=
+{
+  pars0 :> params0;
+  localsT: Type[0]
+}.
 \end{lstlisting}
 Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
@@ -261 +263 @@
 Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
 \begin{lstlisting}
-record params (globals: list ident): Type[1] ≝
- { succ_ : Type[0]
- ; pars1 :> params1
- ; codeT: Type[0]
- ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
- }.
+record params (globals: list ident): Type[1] :=
+{
+  succ_ : Type[0];
+  pars1 :> params1;
+  codeT : Type[0];
+  lookup: codeT $\rightarrow$ label $\rightarrow$ option (joint_statement (mk_params_ pars1 succ_) globals)
+}.
 \end{lstlisting}
 We now have what we need to define internal functions for the joint language.
@@ -282 +285 @@
   joint_if_locals   : localsT p;
   joint_if_stacksize: nat;
-  joint_if_code     : codeT … p;
-  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
-  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
+  joint_if_code     : codeT ... p;
+  joint_if_entry    : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?;
+  joint_if_exit     : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?
 }.
 \end{lstlisting}
@@ -293 +296 @@
 ...
 definition ertl_params__: params__ :=
- mk_params__ register register register register (move_registers × move_registers)
+ mk_params__ register register register register (move_registers $\times$ 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_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).
+  $\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:
@@ -322 +325 @@
   call_dest_for_main: call_dest p;
 
-  succ_pc: succ p → address → res address;
-
-  greg_store_: generic_reg p → beval → regsT → res regsT;
-  greg_retrieve_: regsT → generic_reg p → res beval;
-  acca_store_: acc_a_reg p → beval → regsT → res regsT;
-  acca_retrieve_: regsT → acc_a_reg p → res beval;
-  ...
-  dpl_store_: dpl_reg p → beval → regsT → res regsT;
-  dpl_retrieve_: regsT → dpl_reg p → res beval;
-  ...
-  pair_reg_move_: regsT → pair_reg p → res regsT;
-  pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
+  succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address;
+
+  greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
+  greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval;
+  acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
+  acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval;
+  ...
+  dpl_store_: dpl_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
+  dpl_retrieve_: regsT $\rightarrow$ dpl_reg p $\rightarrow$ res beval;
+  ...
+  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT;
+  pointer_of_label: label $\rightarrow$ $\Sigma$p:pointer. ptype p = Code
 }.
 \end{lstlisting}
@@ -356 +359 @@
   more_sparams1 :> more_sem_params p;
   fetch_statement:
-    genv … p → state (mk_sem_params … more_sparams1) →
-    res (joint_statement (mk_sem_params … more_sparams1) globals);
+    genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
+    res (joint_statement (mk_sem_params ... more_sparams1) globals);
   ...
   save_frame:
-    address → nat → paramsT … p → call_args p → call_dest p →
-    state (mk_sem_params … more_sparams1) →
-    res (state (mk_sem_params … more_sparams1));
+    address $\rightarrow$ nat $\rightarrow$ paramsT ... p $\rightarrow$ call_args p $\rightarrow$ call_dest p $\rightarrow$
+    state (mk_sem_params ... more_sparams1) $\rightarrow$
+    res (state (mk_sem_params ... more_sparams1));
   pop_frame:
-    genv globals p → state (mk_sem_params … more_sparams1) →
-    res ((state (mk_sem_params … more_sparams1)));
+    genv globals p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
+    res ((state (mk_sem_params ... more_sparams1)));
   ...
   set_result:
-    list val → state (mk_sem_params … more_sparams1) →
-    res (state (mk_sem_params … more_sparams1));
+    list val $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
+    res (state (mk_sem_params ... more_sparams1));
   exec_extended:
-    genv globals p → extend_statements (mk_sem_params … more_sparams1) →
-    succ p → state (mk_sem_params … more_sparams1) →
-    IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
+    genv globals p $\rightarrow$ extend_statements (mk_sem_params ... more_sparams1) $\rightarrow$
+    succ p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
+    IO io_out io_in (trace $\times$ (state (mk_sem_params ... more_sparams1)))
  }.
 \end{lstlisting}
@@ -414 +417 @@
 definition eval_statement:
   ∀globals: list ident.∀p:sem_params2 globals.
-    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
+    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
 ...
 \end{lstlisting}
@@ -469 +472 @@
 definition eval_statement:
   ∀globals: list ident.∀p:sem_params2 globals.
-    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
+    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
 ...
 \end{lstlisting}
@@ -477 +480 @@
 definition eval_statement:
   ∀globals: list ident. ∀p:sem_params2 globals.
-    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
+    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
   $\lambda$globals, p, ge, st.
   ...
   match s with
   | LOAD dst addrl addrh ⇒
-    ! vaddrh $\leftarrow$ dph_retrieve … st addrh;
-    ! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
-    ! vaddr $\leftarrow$ pointer_of_address 〈vaddrl,vaddrh〉;
-    ! v $\leftarrow$ opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
-    ! st $\leftarrow$ acca_store p … dst v st;
-    ! st $\leftarrow$ next … l st ;
+    ! vaddrh $\leftarrow$ dph_retrieve ... st addrh;
+    ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl;
+    ! vaddr $\leftarrow$ pointer_of_address $\langle$vaddrl,vaddrh$\rangle$;
+    ! v $\leftarrow$ opt_to_res ... (msg FailedLoad) (beloadv (m ... st) vaddr);
+    ! st $\leftarrow$ acca_store p ... dst v st;
+    ! st $\leftarrow$ next ... l st ;
       ret ? $\langle$E0, st$\rangle$
 \end{lstlisting}
@@ -494 +497 @@
 \begin{lstlisting}
   ...
-! vaddrh $\leftarrow$ dph_retrieve … st addrh;
-! vaddrl $\leftarrow$ dpl_retrieve … st addrl;
+! vaddrh $\leftarrow$ dph_retrieve ... st addrh;
+! vaddrl $\leftarrow$ dpl_retrieve ... st addrl;
   ...
 \end{lstlisting}
@@ -502 +505 @@
 \begin{lstlisting}
   ...
-  bind (dph_retrieve … st addrh) ($\lambda$vaddrh. bind (dpl_retrieve … st addrl)
+  bind (dph_retrieve ... st addrh) ($\lambda$vaddrh. bind (dpl_retrieve ... st addrl)
     ($\lambda$vaddrl. ...))
 \end{lstlisting}
@@ -596 +599 @@
 \end{table}
 \end{landscape}
-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.
+Here, 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.
 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
 These are computed with \texttt{wc -l}, a standard Unix tool.