%{
== Problem 2: Elimination of Administrative Redices ==

}%
tp : type.
o : tp.
=> : tp -> tp -> tp.           %infix right 3 =>.

exp   : tp -> type.
value : tp -> type.
app   : exp (A => B) -> exp A -> exp B.
lam   : (value A -> exp B) -> value (A => B).
ret   : value A -> exp A.
%block sourceb : some {A : tp} block {x : value A}.
%worlds (sourceb) (exp _) (value _).

contra : type.
cvalue : tp -> type.
capp   : cvalue (A => B) -> cvalue A -> (cvalue B -> contra) -> contra.
clam   : (cvalue A -> (cvalue B -> contra) -> contra) -> cvalue (A => B).
%block targetb1 : some {A : tp} block {x : cvalue A}.
%block targetb2 : some {A : tp} block {y : cvalue A -> contra}.
%worlds (targetb1 | targetb2) (contra) (cvalue _).

cps : value A -> cvalue A -> type.
%mode cps +X1 -X2.

cpse : exp A -> ((cvalue A -> contra) -> contra) -> type.
%mode cpse +X1 -X2.

cps/lam : cps (lam (E : value A -> exp B))
              (clam (E' : cvalue A -> (cvalue B -> contra) -> contra))
              <- ({x:value A}{x':cvalue A} cps x x' -> cpse (E x) (E' x')).
cpse/app : cpse (app (E1:exp (B => A)) (E2:exp B))
                ([c : (cvalue A -> contra)] E1' ([f:cvalue (B => A)]
                                                   E2' ([x:cvalue B]
                                                          capp f x c)))
                <- cpse E1 (E1':(cvalue (B => A) -> contra) -> contra)
                <- cpse E2 (E2':(cvalue B -> contra) -> contra).
cpse/ret : cpse (ret (V:value A)) ([c:(cvalue A -> contra)] c V')
                <- cps V (V':cvalue A).

%block cpsb : some {A : tp} block {x : value A} {x' : cvalue A} {d : cps x x'}.
%worlds (cpsb) (cps _ _) (cpse _ _).
%total (E V) (cps E _) (cpse V _).
%{
}%