POPL Tutorial/cps-ctp

CPS conversion with target types

%% Source types
%sort tp %.
%term o tp %.
%term => %pi tp %-> tp %-> tp %.
%prec %right 3 => %.
%% Destination types
%sort ctp %.
%term co ctp %.
%term cnot %pi ctp %-> ctp %.
%term cand %pi ctp %-> ctp %-> ctp %.
%prec %right 3 cand %.
%% Source expressions and values annotated by the translation of their types.
%sort e {_ ctp} %.
%sort v {_ ctp} %.
%term app %pi (e (cnot (A cand (cnot B)))) %-> (e A) %-> (e B) %.
%term lam %pi (%pi (v A) %-> (e B)) %-> (v (cnot (A cand (cnot B)))) %.
%term inj %pi (v A) %-> (e A) %.
%block sourceb [A ctp] {x v A}%.
%worlds (sourceb) (e _) (v _) %.
%% Destination expression and values annotated by their types.
%sort ce %.
%sort cv {_ ctp} %.
% This is the only kind of conjunction we need but it seems pretty odd.
%term capp %pi (cv A) %-> (cv (cnot B)) %-> (cv (cnot (cnot (A cand (cnot B))))) %.
%term clam %pi (%pi (cv A) %-> (cv (cnot B)) %-> ce) %-> (cv (cnot (A cand (cnot B)))) %.
%term cnoti %pi (%pi (cv A) %-> ce) %-> (cv (cnot A)) %.
%term throw %pi (cv A) %-> (cv (cnot A)) %-> ce %.
%block targetb [A ctp] {x cv A}%.
%worlds (targetb) (ce) (cv _) %.
%sort cps {_ v A} {_ cv A} %.
%mode cps %in %out %.
%sort cpse {_ e A} {_ %pi (cv (cnot A)) %-> ce} %.
%mode cpse %in %out %.
%term cps/lam
  %pi (cps (lam (%the (%pi (v A) %-> (e B)) E)) (clam (%the (%pi (cv A) %-> (cv (cnot B)) %-> ce) E')))
  %<- ({x v A} {x' cv A} %pi (cps x x') %-> (cpse (E x) (E' x'))) %.
%term cpse/app
  %pi (cpse (app (%the (e (cnot (B cand (cnot A)))) E1) (%the (e B) E2)) ([c cv (cnot A)] E2' (cnoti ([arg cv B] E1' (capp arg c)))))
  %<- (cpse E1 (%the (%pi (cv (cnot (cnot (B cand (cnot A))))) %-> ce) E1'))
  %<- (cpse E2 (%the (%pi (cv (cnot B)) %-> ce) E2')) %.
%term cpse/inj
  %pi (cpse (inj (%the (v A) V)) ([c cv (cnot A)] throw V' c))
  %<- (cps V (%the (cv A) V')) %.
%block cpsb [A ctp] {x v A} {x' cv A} {d cps x x'}%.
%worlds (cpsb) (cps _ _) (cpse _ _) %.
%total (E V) (cps E _) (cpse V _) %.