POPL Tutorial/cps

CPS Conversion

%sort tp %.
%term o tp %.
%term => %pi tp %-> tp %-> tp %.
%prec %right 3 => %.
%sort e {_ tp} %.
%sort v {_ tp} %.
%term app %pi (e (A => B)) %-> (e A) %-> (e B) %.
%term lam %pi (%pi (v A) %-> (e B)) %-> (v (A => B)) %.
%term inj %pi (v A) %-> (e A) %.
%block sourceb [A tp] {x v A}%.
%worlds (sourceb) (e _) (v _) %.
%sort ce %.
%sort cv {_ tp} %.
%term capp %pi (cv (A => B)) %-> (cv A) %-> (%pi (cv B) %-> ce) %-> ce %.
%term clam %pi (%pi (cv A) %-> (%pi (cv B) %-> ce) %-> ce) %-> (cv (A => B)) %.
%block targetb1 [A tp] {x cv A}%.
%block targetb2 [A tp] {y %pi (cv A) %-> ce}%.
%worlds (targetb1 targetb2) (ce) (cv _) %.
%sort cps {_ v A} {_ cv A} %.
%mode cps %in %out %.
%sort cpse {_ e A} {_ %pi (%pi (cv A) %-> ce) %-> ce} %.
%mode cpse %in %out %.
%term cps/lam
  %pi (cps (lam E) (clam E'))
  %<- ({x v A} {x' cv A} %pi (cps x x') %-> (cpse (E x) (E' x'))) %.
%term cpse/app
  %pi (cpse (app E1 E2) ([c %pi (cv A) %-> ce] E1' ([w1] E2' ([w2] capp w1 w2 c))))
  %<- (cpse E1 E1')
  %<- (cpse E2 E2') %.
%term cpse/inj %pi (cpse (inj E) ([c %pi (cv A) %-> ce] c E')) %<- (cps E E') %.
%block cpsb [A tp] {x v A} {x' cv A} {d cps x x'}%.
%worlds (cpsb) (cps _ _) (cpse _ _) %.
%total (E V) (cps E _) (cpse V _) %.