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

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:

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

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

@@ -330 +330 @@
 
 \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] :=
 {
@@ -364 +352 @@
 }.
 \end{lstlisting}
+
+The \texttt{state} record holds the current state of the interpreter:
+\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}
+Here \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.
+We use the function \texttt{eval\_statement} to evaluate a single joint statement:
+\begin{lstlisting}
+definition eval_statement:
+  ∀globals: list ident.∀p:sem_params2 globals.
+    genv globals p → state p → IO io_out io_in (trace × (state p)) :=
+...
+\end{lstlisting}
+We examine the type here.
 
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%