Changeset 1403 for Deliverables


Ignore:
Timestamp:
Oct 18, 2011, 3:12:48 PM (8 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

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

    r1402 r1403  
    266266\begin{lstlisting}
    267267record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
    268 { joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    269   joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
    270 (*  joint_if_sig: signature;  -- dropped in front end *)
     268{
     269  joint_if_luniverse: universe LabelTag;
     270  joint_if_runiverse: universe RegisterTag;
    271271  joint_if_result   : resultT p;
    272272  joint_if_params   : paramsT p;
    273273  joint_if_locals   : localsT p;
    274 (*CSC: XXXXX stacksize unused for LTL-...*)
    275274  joint_if_stacksize: nat;
    276275  joint_if_code     : codeT … p;
    277 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    278276  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
    279 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    280277  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
    281278}.
     
    303300\end{lstlisting}
    304301
     302\begin{lstlisting}
     303record more_sem_params (p:params_): Type[1] :=
     304{
     305  framesT: Type[0];
     306  regsT: Type[0];
     307  succ_pc: succ p → address → res address;
     308  greg_store_: generic_reg p → beval → regsT → res regsT;
     309  greg_retrieve_: regsT → generic_reg p → res beval;
     310  acca_store_: acc_a_reg p → beval → regsT → res regsT;
     311  acca_retrieve_: regsT → acc_a_reg p → res beval;
     312  accb_store_: acc_b_reg p → beval → regsT → res regsT;
     313  accb_retrieve_: regsT → acc_b_reg p → res beval;
     314  dpl_store_: dpl_reg p → beval → regsT → res regsT;
     315  dpl_retrieve_: regsT → dpl_reg p → res beval;
     316  dph_store_: dph_reg p → beval → regsT → res regsT;
     317  dph_retrieve_: regsT → dph_reg p → res beval;
     318  pair_reg_move_: regsT → pair_reg p → res regsT;
     319  pointer_of_label: label → $\Sigma$p:pointer. ptype p = Code
     320}.
     321\end{lstlisting}
     322
     323\begin{lstlisting}
     324record sem_params: Type[1] :=
     325{
     326  spp :> params_;
     327  more_sem_pars :> more_sem_params spp
     328}.
     329\end{lstlisting}
     330
     331\begin{lstlisting}
     332record state (p: sem_params): Type[0] :=
     333{
     334  st_frms: framesT ? p;
     335  pc: address;
     336  sp: pointer;
     337  carry: beval;
     338  regs: regsT ? p;
     339  m: bemem
     340}.
     341\end{lstlisting}
     342
     343\begin{lstlisting}
     344record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
     345{
     346  more_sparams1 :> more_sem_params p;
     347  fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals);
     348  fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address);
     349  result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p));
     350  init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1;
     351  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));
     352  pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)));
     353  fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val);
     354  set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1));
     355  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)))
     356 }.
     357\end{lstlisting}
     358
     359\begin{lstlisting}
     360record sem_params2 (globals: list ident): Type[1] :=
     361{
     362  p2 :> params globals;
     363  more_sparams2 :> more_sem_params2 globals p2
     364}.
     365\end{lstlisting}
     366
    305367%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    306368% SECTION.                                                                    %
     
    322384For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
    323385\begin{lstlisting}
     386XXX
    324387\end{lstlisting}
    325388\item
Note: See TracChangeset for help on using the changeset viewer.