Changeset 1405


Ignore:
Timestamp:
Oct 18, 2011, 4:19:33 PM (9 years ago)
Author:
mulligan
Message:

yet more added. apparently there's more parameters than i ever thought imaginable

File:
1 edited

Legend:

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

    r1403 r1405  
    330330
    331331\begin{lstlisting}
    332 record 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}
    344332record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
    345333{
     
    364352}.
    365353\end{lstlisting}
     354
     355The \texttt{state} record holds the current state of the interpreter:
     356\begin{lstlisting}
     357record state (p: sem_params): Type[0] :=
     358{
     359  st_frms: framesT ? p;
     360  pc: address;
     361  sp: pointer;
     362  carry: beval;
     363  regs: regsT ? p;
     364  m: bemem
     365}.
     366\end{lstlisting}
     367Here \texttt{st\_frms} represent stack frames, \texttt{pc} the program counter, \texttt{sp} the stack pointer, \texttt{carry} the carry flag, \texttt{regs} the generic registers and \texttt{m} external RAM.
     368We use the function \texttt{eval\_statement} to evaluate a single joint statement:
     369\begin{lstlisting}
     370definition eval_statement:
     371  ∀globals: list ident.∀p:sem_params2 globals.
     372    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
     373...
     374\end{lstlisting}
     375We examine the type here.
    366376
    367377%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset for help on using the changeset viewer.