Library examples.CPS

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.

Index
This page has been generated by coqdoc