| Translation into the continuation-only language |
Require Import List.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Require Import CTPC.Continuation.
Require Import CTPC.Source.
Require Import CTPC.CPS.
Require Import CTPC.Cont.
Set Implicit Arguments.
Auxiliary syntactic functions |
Definition swap t1 t2 G (lin : olinear (t1 :: t2 :: G) tt) : olinear (t2 :: t1 :: G) tt :=
Olinear.permute nil _ _ _ lin.
Theorem swap_sound : forall t1 t2 G (lin : olinear (t1 :: t2 :: G) tt) x1 x2 s,
olinearDenote (swap lin) (SCons _ x1 (SCons _ x2 s))
= olinearDenote lin (SCons _ x2 (SCons _ x1 s)).
The translation |
Fixpoint contifyTy (t : sty) : oty :=
match t with
| SNat => ONat
| SArrow dom ran => OCont (contifyTy dom :: OCont (contifyTy ran :: nil) :: nil)
end.
Section ifVar.
Variables (G : list sty) (t : sty)
(T : Set) (varCase : Var G t -> T) (defaultCase : T).
Definition ifVar (op : pprimop G t) : T.
Theorem ifVar_sound : forall (P : T -> Prop)
(op : pprimop G t),
(forall v, op = PVar v -> P (varCase v))
-> P defaultCase
-> P (ifVar op).
End ifVar.
Fixpoint contifyPrimop (G : list sty) (t : sty) (op : pprimop G t) {struct op}
: oprimop (map contifyTy G) (contifyTy t) :=
match op in (pprimop G t) return (oprimop (map contifyTy G) (contifyTy t)) with
| PConst _ n => OConst _ n
| PVar _ _ v => OVar (VarConvert _ v)
| PLam _ _ _ lin => OLam (OCCons (OCCons (OCNil (contifyLinear lin))))
end
with contifyLinear (G : list sty) (t : sty) (lin : plinear G t) {struct lin}
: olinear (OCont (contifyTy t :: nil) :: map contifyTy G) tt :=
match lin in (plinear G t) return (olinear (OCont (contifyTy t :: nil) :: map contifyTy G) tt) with
| PThrow _ _ op =>
ifVar
(fun v =>
OApply (First _ _) (OACons (Next _ (VarConvert contifyTy v)) (OANil _)))
(OBind
(Oprimop.lift _ (contifyPrimop op))
(OApply (Next _ (First _ _)) (OACons (First _ _) (OANil _))))
op
| PApply _ _ _ _ func arg cont =>
OBind
(OLam (OCCons (OCNil
(OApply (Next _ (Next _ (VarConvert contifyTy cont)))
(OACons (First _ _)
(OACons (Next _ (First _ _))
(OANil _)))))))
(OApply
(Next _ (Next _ (VarConvert contifyTy func)))
(OACons (Next _ (Next _ (VarConvert _ arg)))
(OACons (First _ _)
(OANil _))))
| PBind _ _ _ op lin' =>
OBind
(Oprimop.lift _ (contifyPrimop op))
(swap (contifyLinear lin'))
end.
Logical relations |
Fixpoint val_lr (t : sty) : ptyDenote t -> otyDenote (contifyTy t) -> Prop :=
match t return (ptyDenote t -> otyDenote (contifyTy t) -> Prop) with
| SNat => fun ns no => ns = no
| SArrow dom ran => fun fp fo =>
forall xp xo, val_lr dom xp xo
-> exists thrownp,
(forall k, fp xp k = k thrownp)
/\ exists throwno,
(forall k, fo (xo, (k, tt)) = k (throwno, tt))
/\ val_lr ran thrownp throwno
end.
Definition Subst_lr := Subst_lr contifyTy val_lr.
Hint Unfold Subst_lr.
Definition primop_lr G t (opp : pprimop G t) (opo : oprimop (map contifyTy G) (contifyTy t)) :=
forall s s', Subst_lr s s'
-> val_lr t (pprimopDenote opp s) (oprimopDenote opo s').
Definition linear_lr G t (linp : plinear G t) (lino : olinear (OCont (contifyTy t :: nil) :: map contifyTy G) tt) :=
forall s s', Subst_lr s s'
-> exists thrownp,
(forall k, plinearDenote linp s k = k thrownp)
/\ exists throwno,
(forall k, olinearDenote lino (SCons _ k s') = k (throwno, tt))
/\ val_lr t thrownp throwno.
Soundness proof |
Scheme pprimop_scheme := Induction for pprimop Sort Prop
with plinear_scheme := Induction for plinear Sort Prop.
Lemma oprimop_lift_sound : forall (G : list oty) (t : oty) (e : oprimop G t) (t' : oty),
oprimopDenote (Oprimop.lift t' e) = fun s => oprimopDenote e (tail s).
Hint Rewrite oprimop_lift_sound swap_sound : Contify.
Ltac my_simpl := unfold linear_lr, primop_lr, withCont_bind, withCont_compose in *;
fold ptyDenote in *; fold otyDenote in *; fold contifyTy in *;
autorewrite with Contify; try apply ifVar_sound.
Ltac my_lr_tac := lr_tac ltac:(var_adder val_lr) stricter_inster my_simpl.
Theorem contifyLinear_sound : forall G t (e : plinear G t),
linear_lr e (contifyLinear e).