POPL Tutorial/cps-rp

%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 ctp %.
%term co ctp %.
%term carr %pi ctp %-> ctp %-> ctp %.
%sort ce %.
%sort cv {_ ctp} %.
%term capp %pi (cv (carr A B)) %-> (cv A) %-> (%pi (cv B) %-> ce) %-> ce %.
%term clam %pi (%pi (cv A) %-> (%pi (cv B) %-> ce) %-> ce) %-> (cv (carr A B)) %.
%block targetb1 [A ctp] {x cv A}%.
%block targetb2 [A ctp] {y %pi (cv A) %-> ce}%.
%worlds (targetb1 targetb2) (ce) (cv _) %.
%sort trans-tp {_ tp} {_ ctp} %.
%term trans-tp/o trans-tp o co %.
%term trans-tp/arr %pi (trans-tp (T1 => T2) (carr P1 P2)) %<- (trans-tp T1 P1) %<- (trans-tp T2 P2) %.
%sort can-trans-tp {A tp} {_ trans-tp A A'} %.
%mode can-trans-tp %in %out %.
%term _ can-trans-tp _ trans-tp/o %.
%term _
  %pi (can-trans-tp (A => B) (trans-tp/arr D2 D1))
  %<- (can-trans-tp A D1)
  %<- (can-trans-tp B D2) %.
%worlds () (can-trans-tp _ _) %.
%total (D1) (can-trans-tp D1 _) %.
%sort ctp-eq {_ ctp} {_ ctp} %.
%term ctp-eq/i ctp-eq A' A' %.
%sort ctp-eq-resp {C %pi ctp %-> ctp %-> ctp} {_ ctp-eq A1 A1'} {_ ctp-eq A2 A2'} {_ ctp-eq (C A1 A2) (C A1' A2')} %.
%mode ctp-eq-resp %in %in %in %out %.
%term _ ctp-eq-resp C (%the (ctp-eq A A) ctp-eq/i) (%the (ctp-eq B B) ctp-eq/i) (%the (ctp-eq (C A B) (C A B)) ctp-eq/i) %.
%worlds () (ctp-eq-resp _ _ _ _) %.
%total {} (ctp-eq-resp _ _ _ _) %.
%sort trans-tp-unique {_ trans-tp A A'} {_ trans-tp A A''} {_ ctp-eq A' A''} %.
%mode trans-tp-unique %in %in %out %.
%term _ trans-tp-unique trans-tp/o trans-tp/o ctp-eq/i %.
%term _
  %pi (trans-tp-unique (trans-tp/arr D2 D1) (trans-tp/arr D2' D1') DQ3)
  %<- (trans-tp-unique D1 D1' DQ1)
  %<- (trans-tp-unique D2 D2' DQ2)
  %<- (ctp-eq-resp carr DQ1 DQ2 DQ3) %.
%worlds () (trans-tp-unique _ _ _) %.
%total (D1) (trans-tp-unique D1 _ _) %.
%sort ceo-resp-ctp-eq {_ ctp-eq A A'} {_ %pi (%pi (cv A) %-> ce) %-> ce} {_ %pi (%pi (cv A') %-> ce) %-> ce} %.
%mode ceo-resp-ctp-eq %in %in %out %.
%term _ ceo-resp-ctp-eq _ D1 D1 %.
%worlds (targetb1 targetb2) (ceo-resp-ctp-eq _ _ _) %.
%total {} (ceo-resp-ctp-eq _ _ _) %.
%sort cps {_ v A} {_ trans-tp A A'} {_ cv A'} %.
%mode cps %in %out %out %.
%sort cpse {_ e A} {_ trans-tp A A'} {_ %pi (%pi (cv A') %-> ce) %-> ce} %.
%mode cpse %in %out %out %.
%sort cpse+ {_ e A} {_ trans-tp A A'} {_ %pi (%pi (cv A') %-> ce) %-> ce} %.
%mode cpse+ %in %in %out %.
%term cps/lam
  %pi (cps (lam E) (trans-tp/arr D2 D1) (clam E'))
  %<- (can-trans-tp _ D1)
  %<- ({x v A} {x' cv A'} %pi (cps x D1 x') %-> (cpse (E x) D2 (E' x'))) %.
%term cpse/app
  %pi (cpse (app E1 E2) D2 ([c %pi (cv A') %-> ce] E1' ([w1] E2' ([w2] capp w1 w2 c))))
  %<- (cpse E1 (trans-tp/arr D2 D1) E1')
  %<- (cpse+ E2 D1 E2') %.
%term cpse/inj %pi (cpse (inj E) D1 ([c %pi (cv A) %-> ce] c E')) %<- (cps E D1 E') %.
%term cpse+/i
  %pi (cpse+ E D1 E'')
  %<- (cpse E D1' E')
  %<- (trans-tp-unique D1' D1 DQ)
  %<- (ceo-resp-ctp-eq DQ E' E'') %.
%block cpsb [A tp] [A' ctp] [D1 trans-tp A A'] {x v A} {x' cv A'} {d cps x D1 x'}%.
%worlds (cpsb) (cps _ _ _) (cpse _ _ _) (cpse+ _ _ _) %.
%total (E V E') (cps E _ _) (cpse V _ _) (cpse+ E' _ _) %.