Changeset 1403 for Deliverables/D4.2-4.3

Timestamp:

Oct 18, 2011, 3:12:48 PM (8 years ago)

Author:

mulligan

Message:

more added

File:

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

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

@@ -266 +266 @@
 \begin{lstlisting}
 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
-{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
-  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
-(*  joint_if_sig: signature;  -- dropped in front end *)
+{
+  joint_if_luniverse: universe LabelTag;
+  joint_if_runiverse: universe RegisterTag;
   joint_if_result   : resultT p;
   joint_if_params   : paramsT p;
   joint_if_locals   : localsT p;
-(*CSC: XXXXX stacksize unused for LTL-...*)
   joint_if_stacksize: nat;
   joint_if_code     : codeT … p;
-(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
   joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
-(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
   joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
 }.
@@ -303 +300 @@
 \end{lstlisting}
 
+\begin{lstlisting}
+record more_sem_params (p:params_): Type[1] :=
+{
+  framesT: Type[0];
+  regsT: Type[0];
+  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;
+  accb_store_: acc_b_reg p → beval → regsT → res regsT;
+  accb_retrieve_: regsT → acc_b_reg p → res beval;
+  dpl_store_: dpl_reg p → beval → regsT → res regsT;
+  dpl_retrieve_: regsT → dpl_reg p → res beval;
+  dph_store_: dph_reg p → beval → regsT → res regsT;
+  dph_retrieve_: regsT → dph_reg p → res beval;
+  pair_reg_move_: regsT → pair_reg p → res regsT;
+  pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
+}.
+\end{lstlisting}
+
+\begin{lstlisting}
+record sem_params: Type[1] :=
+{
+  spp :> params_;
+  more_sem_pars :> more_sem_params spp
+}.
+\end{lstlisting}
+
+\begin{lstlisting}
+record state (p: sem_params): Type[0] :=
+{
+  st_frms: framesT ? p;
+  pc: address;
+  sp: pointer;
+  carry: beval;
+  regs: regsT ? p;
+  m: bemem
+}.
+\end{lstlisting}
+
+\begin{lstlisting}
+record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
+{
+  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);
+  fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address);
+  result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p));
+  init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1;
+  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));
+  pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)));
+  fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val);
+  set_result: list val → state (mk_sem_params … more_sparams1) → 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)))
+ }.
+\end{lstlisting}
+
+\begin{lstlisting}
+record sem_params2 (globals: list ident): Type[1] :=
+{
+  p2 :> params globals;
+  more_sparams2 :> more_sem_params2 globals p2
+}.
+\end{lstlisting}
+
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
 % SECTION.                                                                    %
@@ -322 +384 @@
 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
 \begin{lstlisting}
+XXX
 \end{lstlisting}
 \item