%%% Operational semantics

%%% Version 1: straightforward, big-step
%%% Using intrinsically typed terms
%%% Avoids run-time artefacts

%%% Definitions for term syntax
lam = =>I.
app = =>E.
box = !I.
unbox = !E.
fetch = ([W'] !G : ! A @ W' -> ! A @ W).
here = ?I.
letd = ?E.
get = ([W'] ?G : ? A @ W' -> ? A @ W).

%%% Values
value : {W:world} A @ W -> type.	%name value Q.
%mode value +W +V.
val_lam : value W (lam [x] M x).
val_box : value W (fetch W' (box [o] M o)).
val_here : value W (get W' (here V'))
	    <- value W' V'.

%%% Evaluation (big-step)
eval : {W:world} A @ W -> A @ W -> type. %name eval D.
%mode eval +W +M -V.
ev_lam : eval W (lam [x] M x) (lam [x] M x).
ev_app : eval W (app M1 M2) V
	  <- eval W M1 (lam [x] M1' x)
	  <- eval W M2 V2
	  <- eval W (M1' V2) V.
ev_box : eval W (box [o] M o) (fetch W (box [o] M o)).
ev_unbox : eval W (unbox M1) V
	    <- eval W M1 (fetch W' (box [o] M1' o))
	    <- eval W (M1' W) V.
ev_fetch : eval W (fetch W' M') (fetch W'' (box [o] M'' o))
	    <- eval W' M' (fetch W'' (box [o] M'' o)).
ev_here : eval W (here M1) (get W (here V1))
	   <- eval W M1 V1.
ev_letd : eval W (letd M1 ([o] [x:A1 @ o] M2 o x)) V
	    <- eval W M1 (get W' (here V1'))
	    <- eval W (M2 W' V1') V.
ev_get : eval W (get W' M') (get W'' (here V''))
	  <- eval W' M' (get W'' (here V'')).
%worlds () (eval W M V).
%covers eval +W +M -V.

%%% Value soundness
%%% (evaluation returns a value) 
vs : eval W M V -> value W V -> type.
%mode vs +D -Q.
vs_lam : vs (ev_lam) (val_lam).
vs_app : vs (ev_app D1' D2 D1) Q
	  <- vs D1' Q.
vs_box : vs (ev_box) (val_box).
vs_unbox : vs (ev_unbox D1' D1) Q
	    <- vs D1' Q.
vs_fetch : vs (ev_fetch D') (val_box)
	    <- vs D' (val_box).
vs_here : vs (ev_here D1) (val_here Q1)
	   <- vs D1 Q1.
vs_letd : vs (ev_letd D2 D1) Q
	   <- vs D2 Q.
vs_get : vs (ev_get D') (val_here Q'')
	  <- vs D' (val_here Q'').
%worlds () (vs D Q).
%total D (vs D Q).

%%% Version 2
%%% Small-step semantics
%%% Values, frames, and continuations as run-time artefacts
%%% No tables (using substitution instead)
%%% Final answer type and world is not (yet) represented.

% Values
# : prop -> world -> type.		%name # V.
%infix none 1 #.

vlam : (A @ W -> B @ W) -> A => B # W.	% lam ([x] M x)
vbox : ({o:world} A @ o) -> ! A # W.	% fetch _ (box [o] M o)
vhere : {W':world} A # W' -> ? A # W.	% get W' (here V)

% Inclusion of values in expressions
val : A # W -> A @ W.

% Frames
% frame A W C W' maps values A # W to continuations C at W
frame : prop -> world -> prop -> world -> type.	%name frame F.

app1 : A @ W -> frame (A => B) W B W.	    % app1 M2 ~ [v1] app v1 M2
app2 : A => B # W -> frame A W B W.	    % app2 V1 ~ [v2] app V1 v2
unbox1 : frame (! A) W A W.		    % unbox1  ~ [v] unbox v
fetch1 : {W':world} frame (! A) W' (! A) W. % fetch1 W' ~ [v'] fetch W' v'
here1 : frame A W (? A) W.		    % here1 ~ [v] here1 v
letd1 : ({o:world} A @ o -> C @ W) -> frame (? A) W C W.
                   % letd1 ([o][x] M2 o x) ~ [v1] letd v1 ([o] [x] M2 o x)
get1 : {W':world} frame (? A) W' (? A) W.   % get1 W' ~ [v'] get W' v'

% Continuations
cont : prop -> world -> type.		%name cont K.
finish : cont A W.
; : cont C W' -> frame A W C W' -> cont A W.
%infix none 1 ;.

% Instructions
inst : prop -> world -> type.		%name inst I.
ev : A @ W -> inst A W.
ret : A # W -> inst A W.

% States
state : prop -> world -> type.		%name state S.
st : {W:world} cont A W -> inst A W -> state A W.

% Single step
% Only fetch, fetch1 and get, get1 change current world
step : state A W -> state A' W' -> type.
%mode step +S -S'.

st_val :    step (st W (K) (ev (val V)))
                 (st W (K) (ret V)).

st_app :    step (st W (K) (ev (app M1 M2)))
                 (st W (K ; app1 M2) (ev M1)).
st_app1 :   step (st W (K ; app1 M2) (ret V1))
	         (st W (K ; app2 V1) (ev M2)).
st_app2 :   step (st W (K ; app2 (vlam [x] M1' x)) (ret V2))
                 (st W (K) (ev (M1' (val V2)))).
st_lam :    step (st W (K) (ev (lam [x] M x)))
	         (st W (K) (ret (vlam [x] M x))).

st_box :    step (st W (K) (ev (box [o] M o)))
	         (st W (K) (ret (vbox [o] M o))).
st_unbox :  step (st W (K) (ev (unbox M)))
                 (st W (K ; unbox1) (ev M)).
st_unbox1 : step (st W (K ; unbox1) (ret (vbox [o] M o)))
	         (st W (K) (ev (M W))).
st_fetch :  step (st W (K) (ev (fetch W' M')))
	         (st W' (K ; fetch1 W') (ev M')).
st_fetch1 : step (st W' (K ; fetch1 W') (ret (vbox [o] M' o)))
	         (st W (K) (ret (vbox [o] M' o))).

st_here :   step (st W (K) (ev (here M)))
	         (st W (K ; here1) (ev M)).
st_here1 :  step (st W (K ; here1) (ret V))
                 (st W (K) (ret (vhere W V))).
st_letd :   step (st W (K) (ev (letd M1 ([o] [x] M2 o x))))
	         (st W (K ; letd1 ([o] [x] M2 o x)) (ev M1)).
st_letd1 :  step (st W (K ; letd1 ([o] [x] M2 o x)) (ret (vhere W' V1')))
	         (st W (K) (ev (M2 W' (val V1')))).
st_get :    step (st W (K) (ev (get W' M)))
 	         (st W' (K ; get1 W') (ev M)).
st_get1 :   step (st W' (K ; get1 W') (ret (vhere W'' V)))
	         (st W (K) (ret (vhere W'' V))).

% Last case to verify progress
st_halt :   step (st W (finish) (ret V))
                 (st W (finish) (ret V)).

% Allow world parameters, otherwise totality is trivial
%worlds (lo) (step S S').
%total [] (step S S').