| Target language of closure conversion from CPS form |
Require Import Bool List TheoryList.
Require Import LambdaTamer.LambdaTamer.
Require Import CTPC.Continuation.
Set Implicit Arguments.
Type language |
| Compared to the previous languages, we add a type of code annotated with an environment record type. Values of arrow type are formed by applying values of code types to appropriate environment records. |
Syntax |
Inductive cty : Set :=
| CNat : cty
| CCont : list cty -> cty
| CProd : list cty -> cty
| CCode : list cty -> list cty -> cty.
Definition ctys := list cty.
Record cprojTy : Set := {
ctFields : ctys;
ctChosen : cty
}.
Denotational semantics |
Fixpoint ctyDenote (t : cty) : Set :=
match t with
| CNat => nat
| CCont args =>
(fix ctysDenote (ts : ctys) : Set :=
match ts with
| nil => unit
| t :: ts' => (ctyDenote t * ctysDenote ts')%type
end) args -> result
| CProd ts =>
(fix ctysDenote (ts : ctys) : Set :=
match ts with
| nil => unit
| t :: ts' => (ctyDenote t * ctysDenote ts')%type
end) ts
| CCode ctx args =>
(fix ctysDenote (ts : ctys) : Set :=
match ts with
| nil => unit
| t :: ts' => (ctyDenote t * ctysDenote ts')%type
end) ctx
* (fix ctysDenote (ts : ctys) : Set :=
match ts with
| nil => unit
| t :: ts' => (ctyDenote t * ctysDenote ts')%type
end) args
-> result
end.
Fixpoint ctysDenote (ts : ctys) : Set :=
match ts with
| nil => unit
| t :: ts' => (ctyDenote t * ctysDenote ts')%type
end.
Definition cresultDenote (_ : unit) := result.
Definition cfuncTyDenote (args : ctys) := ctysDenote args -> result.
Definition cprojTyDenote (p : cprojTy) := ctysDenote (ctFields p) -> ctyDenote (ctChosen p).
Definition isSmall' (t : cty) :=
match t with
| CCode _ _ => false
| _ => true
end.
Fixpoint isSmalls' (ts : ctys) : bool :=
match ts with
| nil => true
| t :: s => isSmall' t && isSmalls' s
end.
Definition isSmall t := isSmall' t = true.
Definition isSmalls ts := isSmalls' ts = true.
Definition smallCty := sig isSmall.
Definition smallCtys := sig isSmalls.
Term language |
Syntax |
Inductive cargs : list cty -> ctys -> Set :=
| CANil : forall G, cargs G nil
| CACons : forall G t ts,
Var G t
-> cargs G ts
-> cargs G (t :: ts)
with cproj : list cty -> cprojTy -> Set :=
| CPFst : forall G t ts,
cproj G (Build_cprojTy (t :: ts) t)
| CPSnd : forall G t t' ts,
cproj G (Build_cprojTy ts t)
-> cproj G (Build_cprojTy (t' :: ts) t)
with cprimop : list cty -> cty -> Set :=
| CVar : forall G (t : smallCty),
Var G (proj1_sig t)
-> cprimop G (proj1_sig t)
| CConst : forall G, nat -> cprimop G CNat
| CClosure : forall G (ctx : smallCtys) args,
Var G (CCode (proj1_sig ctx) args)
-> cargs G (proj1_sig ctx)
-> cprimop G (CCont args)
| CProj : forall G ts t,
Var G (CProd ts)
-> cproj G (Build_cprojTy ts t)
-> cprimop G t
with clinear : list cty -> unit -> Set :=
| CApply : forall G (args : smallCtys),
Var G (CCont (proj1_sig args))
-> cargs G (proj1_sig args)
-> clinear G tt
| CBind : forall G (t : smallCty),
cprimop G (proj1_sig t)
-> clinear (proj1_sig t :: G) tt
-> clinear G tt
with cfunc : list cty -> ctys -> Set :=
| CFBody : forall G,
clinear G tt
-> cfunc G nil
| CFLam : forall G (t : smallCty) ctx,
cfunc (proj1_sig t :: G) ctx
-> cfunc G (proj1_sig t :: ctx)
with cfuncs : list cty -> ctys -> Set :=
| CFNil : forall G, cfuncs G nil
| CFCons : forall G ctx args ts,
cfunc G (CProd ctx :: args)
-> cfuncs (CCode ctx args :: G) ts
-> cfuncs G (CCode ctx args :: ts).
Denotational semantics |
Fixpoint cargsDenote G ctx (e : cargs G ctx) {struct e}
: Subst ctyDenote G -> ctysDenote ctx :=
match e in (cargs G ctx) return (Subst ctyDenote G -> ctysDenote ctx) with
| CANil _ => fun _ => tt
| CACons _ _ _ v e' => fun s => (VarDenote v s, cargsDenote e' s)
end
with cprojDenote G pt (e : cproj G pt) {struct e}
: Subst ctyDenote G -> cprojTyDenote pt :=
match e in (cproj G pt) return (Subst ctyDenote G -> cprojTyDenote pt) with
| CPFst _ _ _ => fun _ args => fst args
| CPSnd _ _ _ _ e' => fun s args => cprojDenote e' s (snd args)
end
with cprimopDenote (G : list cty) (t : cty) (op : cprimop G t) {struct op}
: Subst ctyDenote G -> ctyDenote t :=
match op in (cprimop G t) return (Subst ctyDenote G -> ctyDenote t) with
| CVar _ _ v => VarDenote v
| CConst _ n => fun _ => n
| CClosure _ _ _ f e => fun s args => (VarDenote f s) (cargsDenote e s, args)
| CProj _ _ _ p n => fun s => (cprojDenote n s) (VarDenote p s)
end
with clinearDenote (G : list cty) (t : unit) (lin : clinear G t) {struct lin}
: Subst ctyDenote G -> cresultDenote t :=
match lin in (clinear G t) return (Subst ctyDenote G -> cresultDenote t) with
| CApply _ _ func args => fun s =>
(VarDenote func s) (cargsDenote args s)
| CBind _ _ op lin' => fun s =>
withCont_bind
(cprimopDenote op s)
(fun res => clinearDenote lin' (SCons _ res s))
end
with cfuncDenote (G : list cty) (ct : ctys) (cf : cfunc G ct) {struct cf}
: Subst ctyDenote G -> cfuncTyDenote ct :=
match cf in (cfunc G ct)
return (Subst ctyDenote G -> cfuncTyDenote ct) with
| CFBody _ lin => fun s _ => clinearDenote lin s
| CFLam _ _ _ cf' => fun s env => cfuncDenote cf' (SCons _ (fst env) s) (snd env)
end
with cfuncsDenote (G : list cty) (ts : ctys) (fs : cfuncs G ts) {struct fs}
: Subst ctyDenote G -> ctysDenote ts :=
match fs in (cfuncs G ts) return (Subst ctyDenote G -> ctysDenote ts) with
| CFNil _ => fun _ => tt
| CFCons _ _ _ _ cf fs' => fun s =>
withCont_bind
(cfuncDenote cf s)
(fun fd =>
(fd,
cfuncsDenote fs' (SCons (denote:= ctyDenote) (CCode _ _) fd s)))
end.
Programs |
Fixpoint ctysSubst (ts : ctys) : ctysDenote ts -> Subst ctyDenote ts :=
match ts return (ctysDenote ts -> Subst ctyDenote ts) with
| nil => fun _ => SNil _
| t :: ts' => fun vs => SCons _ (fst vs) (ctysSubst _ (snd vs))
end.
Implicit Arguments ctysSubst [ts].
Section cwithProg.
Variable ty : Set.
Variable term : list cty -> ty -> Set.
Record cwithProg (G : list cty) (t : ty) : Set := {
cFns : ctys;
cDefs : cfuncs nil cFns;
cBody : term (G ++ cFns) t
}.
Variable tyDenote : ty -> Set.
Variable termDenote : forall G t, term G t -> Subst ctyDenote G -> tyDenote t.
Definition cwithProgDenote (G : list cty) (t : ty) (p : cwithProg G t)
: Subst ctyDenote G -> tyDenote t :=
fun s => termDenote (cBody p) (appSubst s (ctysSubst (cfuncsDenote (cDefs p) (SNil _)))).
End cwithProg.
Implicit Arguments Build_cwithProg [term G t cFns].
Implicit Arguments cwithProgDenote [term tyDenote G t].
Definition cprog := cwithProg clinear.
Definition cprogDenote := cwithProgDenote _ clinearDenote.
Generate syntactic support code |
Syntactify cargs.
Syntactify cargsDenote.