Turns out the logic is even more refined than nonassociative ordered logic: there's two classes of hypotheses, continuations and intermediate results, and while the intermediate results form a stack, the continuation is always at the base of it, and there's only ever one of 'em. So I have two sorts of worlds, wd and vd.
Didn't prove that the two translations are inverse, but a sanity check on an example works:
in = (dlam [y] e2r (t2e (dlam [x] e2r (dapp (t2e y) (dapp (t2e y) (t2e x)))))).
%define out = V
%solve _ : cps/t in V.
%define out2 = V
%solve _ : ds/t out V.
== : dt A -> dt A -> type.
refl : == X X.
check : {X}{Y} == X Y -> type.
/ : check in out2 refl.
o : type. % simple types
a : o.
=> : o -> o -> o. %infix right 30 =>.
%name o A.
% Direct-style types
dr : o -> type. % roots
de : o -> type. % expressions
dt : o -> type. % terms
%name dr DR dr.
%name de DE de.
%name dt DT dt.
% Direct-style terms
t2e : dt A -> de A.
e2r : de A -> dr A.
dapp : de (A => B) -> de A -> de B.
dlam : (dt A -> dr B) -> dt (A => B).
% Substructural logic
wd : type. %name wd W w.
vd : type. %name vd V v.
* : wd -> vd -> wd. %infix none 30 *.
% CPS-style types
cr : o -> type. % roots
ce : wd -> type. % expressions
ci : o -> vd -> type. % intermediate value on the stack
ct : o -> type. % closed trivial value
cc : o -> wd -> type. % continuations
%name cr CR r.
%name ce CE e.
%name ct CT t.
%name ci CI i.
%name cc CC c.
% CPS-style terms
klam : ({w} cc A w -> ce w) -> cr A.
kapp : ct A -> cc A W -> ce W.
app : cc B W -> ci (A => B) V1 -> ci A V2 -> ce ((W * V1) * V2).
lam : (ct A -> cr B) -> ct (A => B).
vlam : ({v} ci A v -> ce (W * v)) -> cc A W.
% klam : (cc ->> ce) -> cr
% kapp : ct -> cc ->> ce
% app : cc -o ci ->> ci ->> ce
% lam : (ct -> cr) -> ct
% vlam : (ci ->> ce) -o cc
% CPS translation
cps/r : dr A -> cr A -> type.
cps/e : de A -> cc A W -> ce W -> type.
cps/t : dt A -> ct A -> type.
/ : cps/r (e2r E) (klam E')
<- {wc}{c} cps/e E c (E' wc c).
/ : cps/e (t2e T) C (kapp T' C)
<- cps/t T T'.
/ : cps/e (dapp E1 E2) C E1'
<- ({vf:vd} {f:ci _ vf} cps/e E2 (vlam [vx] [x] app C f x) (E2' vf f))
<- cps/e E1 (vlam [vf] [f] E2' vf f) E1'.
/ : cps/t (dlam R) (lam R')
<- {t:dt A} {t':ct A} {d: cps/t t t'} cps/r (R t) (R' t').
% DS translation
wof : wd -> o -> type.
wof/cons : wof (W * V) A <- wof W A.
ds/r : cr A -> dr A -> type.
ds/e : ce W -> wof W A -> de A -> type.
ds/c : cc B W -> wof W A -> de B -> de A -> type.
ds/t : ct A -> dt A -> type.
ds/i : ci A V -> de A -> type.
pop : wof (W * V) B -> wof W B -> type.
pop/ : pop (wof/cons M) M.
/ : ds/t (lam R) (dlam R')
<- {x:ct A} {x':dt A} {d: ds/t x x'} ds/r (R x) (R' x').
/ : ds/r (klam E') (e2r E)
<- {wc}{c}{d:wof wc _}{d2: {dex} ds/c c d dex dex}
ds/e (E' wc c) d E.
/ : ds/e (kapp V C) M E
<- ds/t V V'
<- ds/c C M (t2e V') E.
/ : ds/e (app C I1 I2) M E
<- pop M M'
<- pop M' M''
<- ds/i I2 E2
<- ds/i I1 E1
<- ds/c C M'' (dapp E1 E2) E.
/ : ds/c (vlam ([vi][i] E vi i)) M (E0 : de B) (E' : de A)
<- {vi}{i}{d:ds/i i E0} ds/e (E vi i) (wof/cons M) E'.
% Theorem: CPS translation is total
%mode
(cps/r +R -R')
(cps/e +E +C -E')
(cps/t +T -T').
%block b1 : some {A:o} block {x:dt A} {x':ct A} {d: cps/t x x'}.
%block b2 : some {A:o} block {vx:vd} {x:ci A vx}.
%block b3 : some {A:o} block {wc:wd} {x:cc A wc}.
%worlds (b1 | b2 | b3)
(cps/r R R')
(cps/e E C E')
(cps/t T T').
%total (R E T)
(cps/r R R')
(cps/e E C E')
(cps/t T T').
% Theorem: DS translation is total
%mode
(ds/r +R -R')
(ds/e +E +M -E')
(ds/c +C +M +E -E')
(ds/t +T -T')
(ds/i +I -E)
(pop +M -M').
%block d1 : some {A:o} block {x:ct A} {x':dt A} {d: ds/t x x'}.
%block d2 : some {A:o} block {wc : wd}{c : cc A wc}{d : wof wc A}{d2: {dex:de A} ds/c c d dex dex}.
%block d3 : some {A:o} {E0:de A} block {vi:vd} {i : ci A vi} {d : ds/i i E0}.
%worlds (d1 | d2 | d3)
(ds/r R R')
(ds/e E M E')
(ds/c C M E E')
(ds/t T T')
(ds/i I E)
(pop M M').
%total (M)
(pop M _).
%total (R E C T I)
(ds/r R _)
(ds/e E _ _)
(ds/c C _ _ _)
(ds/t T _)
(ds/i I _).
