Changeset 1405 for Deliverables/D4.2-4.3/reports/D4-3.tex
- Timestamp:
- Oct 18, 2011, 4:19:33 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1403 r1405 330 330 331 331 \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: bemem340 }.341 \end{lstlisting}342 343 \begin{lstlisting}344 332 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] := 345 333 { … … 364 352 }. 365 353 \end{lstlisting} 354 355 The \texttt{state} record holds the current state of the interpreter: 356 \begin{lstlisting} 357 record 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} 367 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. 368 We use the function \texttt{eval\_statement} to evaluate a single joint statement: 369 \begin{lstlisting} 370 definition 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} 375 We examine the type here. 366 376 367 377 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset
for help on using the changeset viewer.