%%% Contents of a cell

contains: cell -> exp -> type.   %name contains Cn

%{
%mode -contains +C -V
}%

% Only run-time assumptions



%%% Collection of all the cells in the store

collect: store -> type.          %name collect Col

col_empty : collect estore.
col_item  : collect (S and (C == V))
             o- contains C V
             o- collect S.

%{
%mode -collect -S
%lex ASSUME TERMINATION
}%


%%% Reading the value of a cell from the store

read: cell -> exp -> type.       %name read R

read_val  : read C V
             o- contains C V
             o- <T>.

%{
%mode -read +C -V
}%


%%% Evaluation

eval : cont -> instr -> answer -> type.   %name eval E

%{
%mode -eval +C +I -A
%lex C
}%

% Expressions

eval_z        : eval K (ev z) A
               o- eval K (return z) A.
eval_s        : eval K (ev (s E)) A
               o- eval (K - [x:exp] return (s x)) (ev E) A.
eval_case     : eval K (ev (case E E1 E2)) A
               o- eval (K - [x:exp] case* x E1 E2) (ev E) A.
eval_pair     : eval K (ev (pair E1 E2)) A
               o- eval (K - [x:exp] pair* x E2) (ev E1) A.
eval_fst      : eval K (ev (fst E)) A
               o- eval (K - [x:exp] fst* x) (ev E) A.
eval_snd      : eval K (ev (snd E)) A
               o- eval (K - [x:exp] snd* x) (ev E) A.
eval_lam      : eval K (ev (lam E)) A
               o- eval K (return (lam E)) A.
eval_app      : eval K (ev (app E1 E2)) A
               o- eval (K - [x:exp] app* x E2) (ev E1) A.
eval_letval   : eval K (ev (letval E1 E2)) A
               o- eval (K - [x:exp] ev (E2 x)) (ev E1) A.
eval_letname  : eval K (ev (letname E1 E2)) A
               o- eval K (ev (E2 E1)) A.
eval_fix      : eval K (ev (fix E)) A
               o- eval K (ev (E (fix E))) A.

eval_cell     : eval K (ev (rf C)) A
               o- eval K (return (rf C)) A.
eval_ref      : eval K (ev (ref E)) A
               o- eval (K - [x:exp] ref* x) (ev E) A.
eval_deref    : eval K (ev (! E)) A
               o- eval (K - [x:exp] deref* x) (ev E) A.
eval_noop     : eval K (ev noop) A
               o- eval K (return noop) A.
eval_seq      : eval K (ev (E1 ; E2)) A
               o- eval (K - [x:exp] ev E2) (ev E1) A.
eval_assign   : eval K (ev (E1 is E2)) A
               o- eval (K - [x:exp] x is*1 E2) (ev E1) A.


% Values

eval_init     : eval init (return V) (close S V)
               o- collect S.
eval_cont     : eval (K - I) (return V) A
               o- eval K (I V) A.


% Auxiliary instructions

eval_case*1   : eval K (case* z E1 E2) A
               o- eval K (ev E1) A.
eval_case*2   : eval K (case* (s V) E1 E2) A
               o- eval K (ev (E2 V)) A.
eval_pair*    : eval K (pair* V E) A
               o- eval (K - [x:exp] return (pair V x)) (ev E) A.
eval_fst*     : eval K (fst* (pair V1 V2)) A
               o- eval K (return V1) A.
eval_snd*     : eval K (snd* (pair V1 V2)) A
               o- eval K (return V2) A.
eval_app*     : eval K (app* (lam E1) E2) A
               o- eval (K - [x:exp] ev (E1 x)) (ev E2) A.

eval_ref*     : eval K (ref* V) (new A)
               o- ({c:cell} contains c V -o eval K (return (rf c)) (A c)).
eval_deref*   : eval K (deref* (rf C)) A
               o- read C V
               &  eval K (return V) A.
eval_assign*1 : eval K ((rf C) is*1 E) A
               o- eval (K - [x:exp] (rf C) is*2 x) (ev E) A.
eval_assign*2 : eval K ((rf C) is*2 V) A
               o- contains C V'
               o- (contains C V -o eval K (return noop) A).