POPL Tutorial/CPS Solution2

Problem 2: Elimination of Administrative Redices

%sort tp %.
%term o tp %.
%term => %pi tp %-> tp %-> tp %.
%prec %right 3 => %.
%sort exp {_ tp} %.
%sort value {_ tp} %.
%term app %pi (exp (A => B)) %-> (exp A) %-> (exp B) %.
%term lam %pi (%pi (value A) %-> (exp B)) %-> (value (A => B)) %.
%term ret %pi (value A) %-> (exp A) %.
%block sourceb [A tp] {x value A}%.
%worlds (sourceb) (exp _) (value _) %.
%sort contra %.
%sort cvalue {_ tp} %.
%term capp %pi (cvalue (A => B)) %-> (cvalue A) %-> (%pi (cvalue B) %-> contra) %-> contra %.
%term clam
  %pi (%pi (cvalue A) %-> (%pi (cvalue B) %-> contra) %-> contra)
  %-> (cvalue (A => B)) %.
%block targetb1 [A tp] {x cvalue A}%.
%block targetb2 [A tp] {y %pi (cvalue A) %-> contra}%.
%worlds (targetb1 targetb2) (contra) (cvalue _) %.
%sort cps {_ value A} {_ cvalue A} %.
%mode cps %in %out %.
%sort cpse {_ exp A} {_ %pi (%pi (cvalue A) %-> contra) %-> contra} %.
%mode cpse %in %out %.
%term cps/lam
  %pi (cps (lam (%the (%pi (value A) %-> (exp B)) E)) (clam (%the (%pi (cvalue A) %-> (%pi (cvalue B) %-> contra) %-> contra) E')))
  %<- ({x value A} {x' cvalue A} %pi (cps x x') %-> (cpse (E x) (E' x'))) %.
%term cpse/app
  %pi (cpse (app (%the (exp (B => A)) E1) (%the (exp B) E2)) ([c %pi (cvalue A) %-> contra] E1' ([f cvalue (B => A)] E2' ([x cvalue B] capp f x c))))
  %<- (cpse E1 (%the (%pi (%pi (cvalue (B => A)) %-> contra) %-> contra) E1'))
  %<- (cpse E2 (%the (%pi (%pi (cvalue B) %-> contra) %-> contra) E2')) %.
%term cpse/ret
  %pi (cpse (ret (%the (value A) V)) ([c %pi (cvalue A) %-> contra] c V'))
  %<- (cps V (%the (cvalue A) V')) %.
%block cpsb [A tp] {x value A} {x' cvalue A} {d cps x x'}%.
%worlds (cpsb) (cps _ _) (cpse _ _) %.
%total (E V) (cps E _) (cpse V _) %.