| CPS transform |
Require Import List.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Require Import CTPC.Source.
Require Import CTPC.Continuation.
Require Import CTPC.CPS.
Set Implicit Arguments.
Generic syntactic functions and their soundness proofs |
Definition insert t G t' (lin : plinear (t :: G) t') t'' : plinear (t :: t'' :: G) t' :=
Plinear.lift' (t :: nil) G lin t''.
Lemma insert_sound : forall G t t' t'0 (lin : plinear (t :: G) t'0)
(s : Subst ptyDenote G)
(x : ptyDenote t') (x0 : ptyDenote t),
plinearDenote (insert lin t') (SCons t x0 (SCons t' x s)) =
plinearDenote lin (SCons t x0 s).
Hint Resolve PlinearDenote.lift_sound insert_sound.
The CPS translation |
Fixpoint compose (G : list sty) (t : sty) (lin : plinear G t) {struct lin}
: forall (t' : sty), plinear (t :: G) t' -> plinear G t' :=
match lin in (plinear G t)
return (forall (t' : sty), plinear (t :: G) t' -> plinear G t') with
| PThrow _ _ op => fun _ lin' =>
PBind op lin'
| PApply _ _ _ _ func arg cont => fun _ lin' =>
PBind
(PLam (PBind
(PLam (insert lin' _))
(PApply
(liftVar (liftVar cont _) _)
(Next _ (First _ _))
(First _ _))))
(PApply
(liftVar func _)
(liftVar arg _)
(First _ _))
| PBind _ _ _ op lin' => fun _ lin'' =>
PBind op (compose lin' (insert lin'' _))
end.
Fixpoint cps (G : list sty) (t : sty) (e : sterm G t) {struct e}
: plinear G t :=
match e in (sterm G t) return (plinear G t) with
| SVar _ _ v => PThrow (PVar v)
| SConst _ n => PThrow (PConst _ n)
| SLam _ _ _ e' => PThrow (PLam (cps e'))
| SApp _ _ _ e1 e2 =>
compose (cps e1)
(compose (Plinear.lift _ (cps e2))
(PBind
(PLam (PThrow (PVar (First _ _))))
(PApply
(Next _ (Next _ (First _ _)))
(Next _ (First _ _))
(First _ _))))
end.
Logical relation definitions |
Fixpoint val_lr (t : sty) : styDenote t -> ptyDenote t -> Prop :=
match t return (styDenote t -> ptyDenote t -> Prop) with
| SNat => fun n1 n2 =>
n1 = n2
| SArrow t1 t2 => fun f1 f2 =>
forall x1 x2, val_lr t1 x1 x2
-> forall (k : _ -> result),
exists thrown, f2 x2 k = k thrown
/\ val_lr t2 (f1 x1) thrown
end.
Hint Constructors SubstU_lr.
Definition Subst_lr := SubstU_lr val_lr.
Hint Unfold Subst_lr.
Definition exp_lr G t (e : sterm G t) (lin : plinear G t) :=
forall s s', Subst_lr s s'
-> forall (k : _ -> result),
exists thrown, plinearDenote lin s' k = k thrown
/\ val_lr t (stermDenote e s) thrown.
Lemma Subst_lr_Var : forall G (s : Subst styDenote G) s' t v,
Subst_lr s s'
-> val_lr t (VarDenote v s) (VarDenote v s').
Hint Resolve Subst_lr_Var.
Some tactics and hints |
Ltac my_simpl := (unfold withCont_const, withCont_bind, withCont_compose in * ).
Hint Extern 1 (VarDenote ?A ?B ?C ?D1 = VarDenote ?A ?B ?C ?D2) =>
replace D2 with D1;
[reflexivity
| idtac].
Hint Extern 1 (plinearDenote ?A ?B ?K1 = plinearDenote ?A ?B ?K2) =>
replace K2 with K1;
[reflexivity
| idtac].
Hint Extern 1 (plinearDenote ?A1 ?B1 ?K = plinearDenote ?A2 ?B2 ?K) =>
replace (plinearDenote A1 B1) with (plinearDenote A2 B2);
[reflexivity
| idtac].
Ltac my_equation_tac := equation_tac ltac:my_simpl.
Soundness of
|
Lemma compose_sound : forall (G : list sty) (t : sty) (lin : plinear G t)
(t' : sty) (lin' : plinear (t :: G) t') s (k : _ -> result),
plinearDenote (compose lin lin') s k
= plinearDenote lin s (fun x => plinearDenote lin' (SCons _ x s) k).
Soundness of
|
Ltac my_rewriter :=
repeat (rewrite compose_sound
|| match goal with
| [ H : _ |- _ ] =>
rewrite compose_sound in H
|| rewrite PlinearDenote.lift_sound in H
end).
Ltac my_lr_tac := lr_tac ltac:(var_adder val_lr) ltac:default_inster ltac:(my_simpl; my_rewriter).
Theorem cps_sound : forall G t (e : sterm G t),
exp_lr e (cps e).