| A certified CPS transformation for a simply-typed lambda calculus |
Require Import List.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Set Implicit Arguments.
The source language: simply-typed lambda calculus |
Syntax and typing rules (combined via dependent types) |
| Types |
Inductive sty : Set :=
| SBool : sty
| SArrow : sty -> sty -> sty
| SProd : sty -> sty -> sty.
| Terms |
Inductive sterm : list sty -> sty -> Set :=
| SVar : forall G t,
Var G t
-> sterm G t
| SConst : forall G,
bool
-> sterm G SBool
| SLam : forall G dom ran,
sterm (dom :: G) ran
-> sterm G (SArrow dom ran)
| SApp : forall G dom ran,
sterm G (SArrow dom ran)
-> sterm G dom
-> sterm G ran
| SPair : forall G t1 t2,
sterm G t1
-> sterm G t2
-> sterm G (SProd t1 t2)
| SFst : forall G t1 t2,
sterm G (SProd t1 t2)
-> sterm G t1
| SSnd : forall G t1 t2,
sterm G (SProd t1 t2)
-> sterm G t2.
Dynamic semantics |
| Denotation function for types |
Fixpoint styDenote (t : sty) : Set :=
match t with
| SBool => bool
| SArrow t1 t2 => styDenote t1 -> styDenote t2
| SProd t1 t2 => (styDenote t1 * styDenote t2)%type
end.
| Denotation function for terms |
Fixpoint stermDenote (G : list sty) (t : sty) (e : sterm G t) {struct e}
: Subst styDenote G -> styDenote t :=
match e in (sterm G t) return (Subst styDenote G -> styDenote t) with
| SConst _ b => fun _ => b
| SVar _ _ v => VarDenote v
| SLam _ _ _ e' => fun s x => stermDenote e' (SCons _ x s)
| SApp _ _ _ e1 e2 => fun s => (stermDenote e1 s) (stermDenote e2 s)
| SPair _ _ _ e1 e2 => fun s => (stermDenote e1 s, stermDenote e2 s)
| SFst _ _ _ e' => fun s => fst (stermDenote e' s)
| SSnd _ _ _ e' => fun s => snd (stermDenote e' s)
end.
Target language: linearized STLC |
Syntax and typing rules |
| Types |
Inductive cty : Set :=
| CBool : cty
| CCont : cty -> cty
| CProd : cty -> cty -> cty.
| Primitive expressions |
Inductive cprimexp : list cty -> cty -> Set :=
| CVar : forall G t,
Var G t
-> cprimexp G t
| CConst : forall G,
bool
-> cprimexp G CBool
| CLam : forall G t,
cexp (t :: G) tt
-> cprimexp G (CCont t)
| CPair : forall G t1 t2,
Var G t1
-> Var G t2
-> cprimexp G (CProd t1 t2)
| CFst : forall G t1 t2,
Var G (CProd t1 t2)
-> cprimexp G t1
| CSnd : forall G t1 t2,
Var G (CProd t1 t2)
-> cprimexp G t2
| Expressions that bind primitive expressions and then call a function |
with cexp : list cty -> unit -> Set :=
| CLet : forall G t,
cprimexp G t
-> cexp (t :: G) tt
-> cexp G tt
| CCall : forall G t,
Var G (CCont t)
-> Var G t
-> cexp G tt.
| Call Lambda Tamer generic programming to build some support code. |
Syntactify cprimexp.
Dynamic semantics |
| Denotation function for types |
Fixpoint ctyDenote (t : cty) : Set :=
match t with
| CBool => bool
| CCont t1 => ctyDenote t1 -> bool
| CProd t1 t2 => (ctyDenote t1 * ctyDenote t2)%type
end.
| Dummy denotation function for the "types" of expressions, which are always unit. The Lambda Tamer generic programming isn't smart enough yet to figure out that such a function is pointless, so we must define it. |
Definition contTy (_ : unit) := bool.
| Another silly definition needed to get around limitations in Syntactify's present understanding of code. |
Definition withCont_bind (A B : Set) (v : A) (f : A -> B) : B :=
f v.
| Denotation functions for expressions |
Fixpoint cprimexpDenote (G : list cty) (t : cty) (e : cprimexp G t) {struct e}
: Subst ctyDenote G -> ctyDenote t :=
match e in (cprimexp G t) return (Subst ctyDenote G -> ctyDenote t) with
| CConst _ b => fun _ => b
| CVar _ _ v => VarDenote v
| CLam _ _ e' => fun s x => cexpDenote e' (SCons _ x s)
| CPair _ _ _ e1 e2 => fun s => (VarDenote e1 s, VarDenote e2 s)
| CFst _ _ _ e' => fun s => fst (VarDenote e' s)
| CSnd _ _ _ e' => fun s => snd (VarDenote e' s)
end
with cexpDenote (G : list cty) (t : unit) (e : cexp G t) {struct e}
: Subst ctyDenote G -> contTy t :=
match e in (cexp G t) return (Subst ctyDenote G -> contTy t) with
| CLet _ _ e1 e2 => fun s =>
withCont_bind
(cprimexpDenote e1 s)
(fun x => cexpDenote e2 (SCons _ x s))
| CCall _ _ f x => fun s => (VarDenote f s) (VarDenote x s)
end.
| Generate lemmas related to these denotation functions. |
Syntactify cprimexpDenote.
The CPS translation |
| It's worth noting that the "type preservation proof" is being written simultaneously with the translation itself, via dependent typing. |
| How to compile a type |
Fixpoint cpsTy (t : sty) : cty :=
match t with
| SBool => CBool
| SArrow t1 t2 => CCont (CProd (cpsTy t1) (CCont (cpsTy t2)))
| SProd t1 t2 => CProd (cpsTy t1) (cpsTy t2)
end.
| Two De Bruijn variable-rearranging helper functions |
Definition insert t G (e : cexp (t :: G) tt) t' : cexp (t :: t' :: G) tt :=
Cexp.lift' (t :: nil) G e t'.
Definition insert2 t1 t2 G (e : cexp (t1 :: t2 :: G) tt) t' : cexp (t1 :: t2 :: t' :: G) tt :=
Cexp.lift' (t1 :: t2 :: nil) G e t'.
| How to compile a term. The return type shows that each compilation expects the most recently bound variable to be a continuation to which it should throw its result. |
Fixpoint cpsTerm (G : list sty) (t : sty) (e : sterm G t) {struct e}
: cexp (CCont (cpsTy t) :: map cpsTy G) tt :=
match e in (sterm G t) return (cexp (CCont (cpsTy t) :: map cpsTy G) tt) with
| SVar _ _ v =>
CCall (First _ _) (liftVar (VarConvert _ v) _)
| SConst _ b =>
CLet
(CConst _ b)
(CCall (Next _ (First _ _)) (First _ _))
| SApp _ _ _ e1 e2 =>
CLet (CLam
(CLet
(CLam
(CLet
(CPair (First _ _) (Next _ (Next _ (First _ _))))
(CCall (Next _ (Next _ (First _ _))) (First _ _))))
(insert (insert (cpsTerm e2) _) _)))
(insert (cpsTerm e1) _)
| SLam _ _ _ e' =>
CLet
(CLam
(CLet
(CFst (First _ _))
(CLet
(CSnd (Next _ (First _ _)))
(insert2 (insert2 (cpsTerm e') _) _))))
(CCall (Next _ (First _ _)) (First _ _))
| SPair _ _ _ e1 e2 =>
CLet (CLam
(CLet
(CLam
(CLet
(CPair (Next _ (First _ _)) (First _ _))
(CCall (Next _ (Next _ (Next _ (First _ _)))) (First _ _))))
(insert (insert (cpsTerm e2) _) _)))
(insert (cpsTerm e1) _)
| SFst _ _ _ e' =>
CLet (CLam
(CLet
(CFst (First _ _))
(CCall (Next _ (Next _ (First _ _))) (First _ _))))
(insert (cpsTerm e') _)
| SSnd _ _ _ e' =>
CLet (CLam
(CLet
(CSnd (First _ _))
(CCall (Next _ (Next _ (First _ _))) (First _ _))))
(insert (cpsTerm e') _)
end.
Semantics preservation proof |
| A logical relation for values, the denotations of terms |
Fixpoint val_lr (t : sty) : styDenote t -> ctyDenote (cpsTy t) -> Prop :=
match t return (styDenote t -> ctyDenote (cpsTy t) -> Prop) with
| SBool => fun b1 b2 => b1 = b2
| SArrow dom ran => fun f1 f2 =>
forall x1 x2, val_lr dom x1 x2
-> exists res, (forall k, f2 (x2, k) = k res)
/\ val_lr ran (f1 x1) res
| SProd t1 t2 => fun p1 p2 =>
val_lr t1 (fst p1) (fst p2)
/\ val_lr t2 (snd p1) (snd p2)
end.
| A logical relation for variable substitutions and an associated hint to the automatic prover |
Definition Subst_lr := Subst_lr cpsTy val_lr.
Hint Unfold Subst_lr.
| A logical relation for terms |
Definition term_lr (G : list sty) (t : sty) (e1 : sterm G t)
(e2 : cexp (CCont (cpsTy t) :: map cpsTy G) tt) : Prop :=
forall s1 s2, Subst_lr s1 s2
-> exists res, (forall k, cexpDenote e2 (SCons _ k s2) = k res)
/\ val_lr t (stermDenote e1 s1) res.
A lemma about insert's commutativity with cexpDenote
|
Definition insert_sound G t t' (e : cexp (t :: G) tt)
(s : Subst ctyDenote G)
(x : ctyDenote t') (x0 : ctyDenote t)
: cexpDenote (insert e t') (SCons t x0 (SCons t' x s)) =
cexpDenote e (SCons t x0 s) :=
CexpDenote.lift'_sound (t :: nil) G e t' (SCons _ x0 s) x.
A lemma about insert2's commutativity with cexpDenote
|
Definition insert2_sound G t1 t2 t' (e : cexp (t1 :: t2 :: G) tt)
(s : Subst ctyDenote G)
(x : ctyDenote t') (x0 : ctyDenote t1) (x1 : ctyDenote t2)
: cexpDenote (insert2 e t') (SCons t1 x0 (SCons t2 x1 (SCons t' x s))) =
cexpDenote e (SCons t1 x0 (SCons t2 x1 s)) :=
CexpDenote.lift'_sound (t1 :: t2 :: nil) G e t'
(SCons _ x0 (SCons _ x1 s)) x.
| Tell the automated prover to try using these lemmas. |
Hint Rewrite insert_sound insert2_sound : CPS.
| Define a task-specific sequent simplification procedure. |
Ltac my_simpl := unfold term_lr, withCont_bind in *;
fold styDenote in *; fold ctyDenote in *; fold cpsTy in *;
| Some rules related to which definitions should be expanded and which definitely shouldn't. |
autorewrite with CPS;
| Call the automatic rewriting procedure |
try match goal with
| [ |- ?F ?X1 = ?F ?X2 ] =>
replace X2 with X1; trivial
end;
| A heuristic for proving that two applications of the same function are equal |
try (apply ext_eq; intro).
| Suggest using extensionality of functions. |
| Define a task-specific procedure for choosing quantifier instantiations. |
Ltac my_inster T k :=
match T with
| (?T1 * ?T2)%type =>
match goal with
| [ H1 : T1, H2 : T2 |- _ ] => k (H1, H2)
end
| To instantiate a quantifier of product type, look for a pair of free variables of the appropriate types. |
| ctyDenote _ * (ctyDenote _ -> bool) -> bool =>
match goal with
| [ e : sterm _ _, s2 : Subst _ _ |- _ ] =>
k (fun p => cexpDenote (cpsTerm e) (SCons _ (snd p) (SCons _ (fst p) s2)))
end
| This rule is hard to describe simply. It's a case that comes up in choosing a continuation for the function abstraction case of the proof. |
| _ => stricter_inster T k
| By default, call an instantiator from the library. |
end.
Use our custom procedures to build a decision procedure using the combinator
lr_tacN, which is specialized to proofs by logical relations.
The first argument specifies how many rounds of a particular simplification
procedure should be run.
|
Ltac my_lr_tac := lr_tacN 3 ltac:(var_adder val_lr) my_inster my_simpl.
| The overall semantics preservation theorem |
Theorem cpsTerm_sound : forall G t (e : sterm G t),
term_lr e (cpsTerm e).
| A proof search hint for the next corollary |
Hint Immediate Slr_Nil.
A specialization of cpsTerm_sound to the boolean type, stated in more
fundamental terms. We consider what happens when we evaluate the
compilation of a boolean expression, where the top-level continuation is
bound to the identity function.
|
Theorem cpsTerm_sound_bool : forall (e : sterm nil SBool),
stermDenote e (SNil _)
= cexpDenote (cpsTerm e) (SCons (denote:= ctyDenote) (CCont CBool) (fun x => x) (SNil _)).
| Output OCaml code equivalent to our certified translation. |
Recursive Extraction cpsTerm.