(*
   Substructural operational semantics
   Call-by-value language with callcc
   Author: Frank Pfenning

   See callcc-trace.lo for a tracing version
*)

exp : type.
dest : type.
frame : type.

eval : exp -> dest -> o.
comp : frame -> dest -> o.
value : dest -> exp -> o.

(* Functions *)
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

app1 : dest -> exp -> frame.
app2 : exp -> dest -> frame.

eval (lam x \ E x) D
  -o {value D (lam x \ E x)}.

eval (app E1 E2) D
  -o {sigma d1 \ eval E1 d1, !comp (app1 d1 E2) D}.

value D1 V1,
comp (app1 D1 E2) D
  -o {sigma d2 \ eval E2 d2, !comp (app2 V1 d2) D}.

value D2 V2,
comp (app2 (lam x \ E1' x) D2) D
  -o {eval (E1' V2) D}.

(* Top-level invocation *)
evaluate : exp -> exp -> o.
evaluate E V o- (pi d0 \ eval E d0 -o {value d0 V}).

(* Test *)
(*
#query 1 2 1
evaluate (app (app (app (lam x \ (lam y \ (lam z \ (app (app x z) (app y z)))))
	                (lam u \ lam v \ u))
                   (lam a \ lam b \ a))
              (lam c \ c))
        V.
*)

(* Mutable store *)
ref : exp -> exp.
deref : exp -> exp.
assign : exp -> exp -> exp.
cell : dest -> exp.		(* new value *)

(* Frames *)
ref1 : dest -> frame.
deref1 : dest -> frame.
assign1 : dest -> exp -> frame.
assign2 : exp -> dest -> frame.

(* ref E, creating cells *)
eval (ref E1) D
  -o {sigma d1 \ eval E1 d1, !comp (ref1 d1) D}.

value D1 V1,
!comp (ref1 D1) D
  -o {sigma c1 \ value c1 V1, value D (cell c1)}.

(* deref E, reading cells *)
eval (deref E1) D
  -o {sigma d1 \ eval E1 d1, !comp (deref1 d1) D}.

value D1 (cell C1),
value C1 V1,
!comp (deref1 D1) D
  -o {value C1 V1, value D V1}.

(* assign E, writing cells *)
eval (assign E1 E2) D
  -o {sigma d1 \ eval E1 d1, !comp (assign1 d1 E2) D}.

value D1 V1,
!comp (assign1 D1 E2) D
  -o {sigma d2 \ eval E2 d2, !comp (assign2 V1 d2) D}.

value D2 V2,
!comp (assign2 (cell C1) D2) D,
value C1 V1
  -o {value C1 V2, value D V2}.

(* Cells are values *)
eval (cell C) D
  -o {value D (cell C)}.

(* Callcc and throw *)
callcc : (exp -> exp) -> exp.
throw : exp -> exp -> exp.
cont : dest -> exp.

throw1 : dest -> exp -> frame.
throw2 : exp -> dest -> frame.

eval (callcc k \ E k) D
  -o {eval (E (cont D)) D}.

eval (throw E1 E2) D
  -o {sigma d1 \ eval E1 d1, !comp (throw1 d1 E2) D}.

value D1 V1,
!comp (throw1 D1 E2) D
  -o {sigma d2 \ eval E2 d2, !comp (throw2 V1 d2) D}.

value D2 (cont D2'),
!comp (throw2 V1 D2) D
  -o {value D2' V1}.

eval (cont D') D
  -o {value D (cont D')}.

(* Evaluation with store cannot return value *)
(* Print value instead, consume store *)
eval_print : exp -> o.

eval_print E
  o- (pi d0 \ eval E d0 -o {sigma V \ value d0 V, write V, nl, top}).

(* Test *)

(* throwing to continuation *)
#query 1 2 1
eval_print
  (app (callcc k \ throw (lam x \ x) k) (lam u \ lam w \ u)).

(* returning to continuation *)
#query 1 2 1
eval_print
  (app (callcc k \ (lam x \ x)) (lam u \ lam w \ u)).

(* first returning then throwing to continuation *)
#query 1 2 1
eval_print
  (app (callcc k \ (lam y \ throw (lam u \ lam w \ w) k))
       (lam z \ z)).