| Closure conversion |
Require Import Eqdep Bool List TheoryList.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Require Import CTPC.Continuation.
Require Import CTPC.Cont.
Require Import CTPC.CC.
Set Implicit Arguments.
Auxiliary types |
Definition cpprog := cwithProg cprimop.
Definition cpprogDenote := cwithProgDenote _ cprimopDenote.
Definition cfprog := cwithProg cfunc.
Definition cfprogDenote := cwithProgDenote _ cfuncDenote.
The closure conversion translation |
Fixpoint ccTy (t : oty) : cty :=
match t with
| ONat => CNat
| OCont args => CCont (map ccTy args)
end.
Definition ccTys := map ccTy.
Theorem ccTySmall : forall t,
isSmall (ccTy t).
Hint Resolve ccTySmall.
Theorem ccTysSmall : forall ts,
isSmalls (map ccTy ts).
Hint Resolve ccTysSmall.
Theorem ccTysViSmall : forall ts vi,
isSmalls (varInfo_apply (map ccTy ts) vi).
Hint Resolve ccTysViSmall.
Fixpoint appCfuncs G ts1 (fs1 : cfuncs G ts1) {struct fs1}
: forall ts2, cfuncs G ts2 -> cfuncs G (ts1 ++ ts2) :=
match fs1 in (cfuncs G ts1) return (forall ts2, cfuncs G ts2 -> cfuncs G (ts1 ++ ts2)) with
| CFNil _ => fun _ fs' => fs'
| CFCons _ _ _ _ f fs' => fun _ fs'' =>
CFCons f (appCfuncs fs' (Cfuncs.lift _ fs''))
end.
Fixpoint bindCfunc (G : list cty) (ts : ctys) (cfs : cfuncs G ts) {struct cfs}
: forall ctx args, cfunc (G ++ ts) (CProd ctx :: args) -> cfuncs G (ts ++ CCode ctx args :: nil) :=
match cfs in (cfuncs G ts)
return (forall ctx args, cfunc (G ++ ts) (CProd ctx :: args)
-> cfuncs G (ts ++ CCode ctx args :: nil)) with
| CFNil _ => fun _ _ cf => Cfuncs.termNil (CFCons cf (CFNil _))
| CFCons _ _ _ _ cf cfs' => fun _ _ cf' =>
CFCons cf (bindCfunc cfs' (Cfunc.front cf'))
end.
Fixpoint ccArgs (G : list oty) (t : otys) (args : oargs G t) {struct args}
: cargs (map ccTy G) (map ccTy t) :=
match args in (oargs G t) return (cargs (map ccTy G) (map ccTy t)) with
| OANil _ => CANil _
| OACons _ _ _ v args' => CACons (VarConvert _ v) (ccArgs args')
end.
Hint Constructors cproj.
Definition grabCproj : forall G0 G' a G,
cproj G0 (Build_cprojTy (G' ++ a :: G) a).
Definition grabCproj'' : forall G0 G' G'0 a G,
cproj G0 (Build_cprojTy (G' +++ G'0 ++ a :: G) a).
Definition grabCproj' : forall G0 G' a G,
cproj G0 (Build_cprojTy (G' +++ a :: G) a).
Definition close'' : forall GG ts (f : cfunc GG ts)
G1 a G G' ftys, GG = G1 ++ a :: G ++ CProd (G' +++ a :: G) :: ftys
-> isSmall a
-> cfunc (G1 ++ G ++ CProd (G' +++ a :: G) :: ftys) ts.
Ltac bool_simpl :=
repeat (match goal with
| [ H : _ |- _ ] =>
(generalize (andb_prop _ _ H)
|| generalize (orb_prop _ _ H));
clear H; intro H
end
|| apply andb_true_intro
|| apply orb_true_intro).
Definition close' : forall (G ts ftys : list cty) G',
isSmalls G
-> cfunc (G ++ CProd (G' +++ G) :: ftys) ts -> cfunc (CProd (G' +++ G) :: ftys) ts.
Definition close : forall (G ts ftys : list cty) (f : cfunc (G ++ ftys) ts),
isSmalls G
-> cfunc ftys (CProd G :: ts).
Implicit Arguments close [G ftys ts].
Fixpoint buildEnv (G : list cty) : forall (vi : varInfo G) ts, cargs (G ++ ts) (varInfo_apply G vi) :=
match G return (forall (vi : varInfo G) ts, cargs (G ++ ts) (varInfo_apply G vi)) with
| nil => fun _ _ => CANil _
| t :: G' => fun vi ts =>
match vi return cargs (t :: G' ++ ts) (varInfo_apply (t :: G') vi) with
| (true, vi') => CACons (First _ _) (Cargs.lift _ (buildEnv _ vi' _))
| (false, vi') => Cargs.lift _ (buildEnv _ vi' _)
end
end.
Fixpoint ccPrimop (G : list oty) (t : oty) (op : oprimop G t) {struct op}
: cpprog (map ccTy G) (ccTy t) :=
match op in (oprimop G t) return cpprog (map ccTy G) (ccTy t) with
| OVar _ _ v => Build_cwithProg _ (CFNil _) (CVar (exist _ _ (ccTySmall _)) (VarNil (VarConvert _ v)))
| OConst _ n => Build_cwithProg _ (CFNil _) (CConst _ n)
| OLam _ _ cont =>
let (ftys, cfs, cont') := ccCont cont in
Build_cwithProg cty (term:= cprimop)
(bindCfunc
cfs (close (ftys:= ftys) (Cfunc.strengthen_app (G1:= nil) cont') (ccTysViSmall _ _)))
(CClosure
(exist _ _ (ccTysViSmall _ _))
(lastVar' _ _ _)
(buildEnv _ _ _))
end
with ccCont (G : list oty) (ts : otys) (cont : ocont G ts) {struct cont}
: cfprog (map ccTy G) (map ccTy ts) :=
match cont in (ocont G ts) return (cfprog (map ccTy G) (map ccTy ts)) with
| OCNil _ lin =>
let (_, cfs, lin') := ccLinear lin in
Build_cwithProg _
cfs
(CFBody lin')
| OCCons _ _ _ cont' =>
let (_, cfs, cont'') := ccCont cont' in
Build_cwithProg _
cfs
(CFLam (exist _ _ (ccTySmall _)) cont'')
end
with ccLinear (G : list oty) (t : unit) (lin : olinear G t) {struct lin}
: cprog (map ccTy G) t :=
match lin in (olinear G t) return (cprog (map ccTy G) t) with
| OApply _ _ f args =>
Build_cwithProg _
(CFNil _)
(CApply
(exist _ _ (ccTysSmall _))
(liftVarEnd _ (VarConvert ccTy f))
(Cargs.liftEnd _ (ccArgs args)))
| OBind _ _ op lin' =>
let (_, cfs1, op') := ccPrimop op in
let (_, cfs2, lin'') := ccLinear lin' in
Build_cwithProg _
(appCfuncs cfs1 cfs2)
(CBind
(exist _ _ (ccTySmall _))
(Cprimop.liftEnd' _ op')
(Clinear.liftMiddle _ lin''))
end.
Logical relations |
Fixpoint val_lr (t : oty) : otyDenote t -> ctyDenote (ccTy t) -> Prop :=
match t return (otyDenote t -> ctyDenote (ccTy t) -> Prop) with
| ONat => fun n1 n2 =>
n1 = n2
| OCont ts => fun f1 f2 =>
forall args1 args2,
(fix vals_lr (ts : otys) : otysDenote ts -> ctysDenote (map ccTy ts) -> Prop :=
match ts return (otysDenote ts -> ctysDenote (map ccTy ts) -> Prop) with
| nil => fun _ _ => True
| t :: ts' => fun a1 a2 =>
val_lr t (fst a1) (fst a2)
/\ vals_lr ts' (snd a1) (snd a2)
end) _ args1 args2
-> f1 args1 = f2 args2
end.
Fixpoint vals_lr (ts : otys) : otysDenote ts -> ctysDenote (map ccTy ts) -> Prop :=
match ts return (otysDenote ts -> ctysDenote (map ccTy ts) -> Prop) with
| nil => fun _ _ => True
| t :: ts' => fun a1 a2 =>
val_lr t (fst a1) (fst a2)
/\ vals_lr ts' (snd a1) (snd a2)
end.
Hint Constructors Subst_lr.
Definition Subst_lr := Subst_lr ccTy val_lr.
Hint Unfold Subst_lr.
Definition primop_lr G t (pop : oprimop G t) (prog : cpprog (map ccTy G) (ccTy t)) :=
forall s s', Subst_lr s s'
-> val_lr t (oprimopDenote pop s) (cpprogDenote prog s').
Definition linear_lr G t (lin : olinear G t) (prog : cprog (map ccTy G) t) :=
forall s s', Subst_lr s s'
-> olinearDenote lin s = cprogDenote prog s'.
Definition cont_lr G ts (cont : ocont G ts) (cont' : cfprog (map ccTy G) (map ccTy ts)) :=
forall s s', Subst_lr s s'
-> forall args1 args2,
vals_lr _ args1 args2
-> ocontDenote cont s args1 = cfprogDenote cont' s' args2.
Definition args_lr G ts (args : oargs G ts) (args' : cargs (map ccTy G) (map ccTy ts)) :=
forall s s', Subst_lr s s'
-> vals_lr ts (oargsDenote args s) (cargsDenote args' s').
Auxiliary soundness lemmas |
Lemma splitCtysSubst : forall G cFns1
(cDefs1 : cfuncs G cFns1) cFns2 (cDefs2 : cfuncs G cFns2) s,
ctysSubst (cfuncsDenote (appCfuncs cDefs1 cDefs2) s)
= appSubst
(ctysSubst (cfuncsDenote cDefs1 s))
(ctysSubst (cfuncsDenote cDefs2 s)).
Definition cfhead : forall G ctx dom ts, cfuncs G (CCode ctx dom :: ts) -> cfunc G (CProd ctx :: dom).
Lemma cast_CFCons : forall G ctx dom (cf : cfunc (G ++ nil) (CProd ctx :: dom)) Heq,
cfhead (eq_rect (G ++ nil) (fun G => cfuncs G _)
(CFCons cf (CFNil _)) G Heq)
= eq_rect _ (fun G => cfunc G _) cf _ Heq.
Lemma invert_cfuncs_nil' : forall (G : list cty) ts
(cfs : cfuncs G ts)
(Heq : nil = ts),
cfs = eq_rect _ (cfuncs G) (CFNil _) _ Heq.
Lemma invert_cfuncs_nil : forall (G : list cty)
(cfs : cfuncs G nil),
cfs = CFNil _.
Lemma invert_cfuncs_cons' : forall (G : list cty) ts
(cfs : cfuncs G ts)
ctx dom (Heq : CCode ctx dom :: nil = ts),
exists cf, cfs = eq_rect _ (cfuncs G) (CFCons cf (CFNil _)) _ Heq.
Lemma invert_cfuncs_cons : forall (G : list cty) ctx dom
(cfs : cfuncs G (CCode ctx dom :: nil)),
exists cf, cfs = CFCons cf (CFNil _).
Lemma bindCfunc_sound : forall G G2 (defs : cfuncs G G2)
(ctx : list cty) (dom : ctys)
(s : Subst ctyDenote G)
(cf : cfunc (G ++ G2) (CProd ctx :: dom)),
ctysSubst
(cfuncsDenote
(bindCfunc defs cf) s)
= appSubst
(ctysSubst (cfuncsDenote defs s))
(SCons (denote:= ctyDenote)
(CCode _ _)
(cfuncDenote cf (appSubst s (ctysSubst (cfuncsDenote defs s))))
(SNil _)).
Lemma closureVar_sound : forall G1 G2 ctx args s defs cf,
VarDenote
(lastVar' G1 G2 (CCode ctx args))
(appSubst s
(ctysSubst
(cfuncsDenote
(bindCfunc defs cf) (SNil _))))
= cfuncDenote cf (ctysSubst (cfuncsDenote defs (SNil _))).
Fixpoint buildEnv' (G : list cty) : forall ts, cargs (G ++ ts) G :=
match G return (forall ts, cargs (G ++ ts) G) with
| nil => fun _ => CANil _
| _ :: _ => fun ts => CACons (First _ _) (Cargs.lift _ (buildEnv' _ _))
end.
Definition ctysDenote_tail : forall ts1 ts2, ctysDenote (ts1 ++ ts2)
-> ctysDenote ts2.
Definition ctysDenote_tail'' : forall ts1 ts1' ts2, ctysDenote (ts1 +++ ts1' ++ ts2)
-> ctysDenote ts2.
Definition ctysDenote_tail' : forall ts1 ts2, ctysDenote (ts1 +++ ts2)
-> ctysDenote ts2.
Definition read_ctys ts1 a ts2 (args : ctysDenote (ts1 ++ a :: ts2))
: ctyDenote a := fst (ctysDenote_tail _ _ args).
Definition read_ctys'' ts1 ts1' a ts2 (args : ctysDenote (ts1 +++ ts1' ++ a :: ts2))
: ctyDenote a := fst (ctysDenote_tail'' _ _ _ args).
Definition read_ctys' ts1 a ts2 (args : ctysDenote (ts1 +++ a :: ts2))
: ctyDenote a := fst (ctysDenote_tail' _ _ args).
Implicit Arguments read_ctys' [ts1 a ts2].
Lemma grabCproj_sound : forall G0 G' a G s args,
cprojDenote (grabCproj G0 G' a G) s args
= read_ctys _ _ _ args.
Lemma grabCproj''_sound : forall G0 G' G'0 a G s args,
cprojDenote (grabCproj'' G0 G' G'0 a G) s args
= read_ctys'' _ _ _ _ args.
Lemma grabCproj'_sound : forall G0 G' a G s args,
cprojDenote (grabCproj' G0 G' a G) s args
= read_ctys' args.
Lemma close''_sound : forall GG ts (f : cfunc GG ts)
G1 a G G' ftys (Heq : GG = G1 ++ a :: G ++ CProd (G' +++ a :: G) :: ftys)
Hsmall s1 s2 x s3 args,
cfuncDenote (close'' f _ _ _ _ Heq Hsmall)
(appSubst s1 (appSubst s2 (SCons _ x s3))) args
= cfuncDenote f
(eq_rect _ (Subst ctyDenote)
(appSubst s1
(SCons _ (read_ctys' x)
(appSubst s2 (SCons _ x s3))))
_ (sym_eq Heq)) args.
Lemma tail_split : forall ts1 ts2 ts3 x Heq,
ctysDenote_tail (ts1 ++ ts2) ts3 x
= ctysDenote_tail _ _
(ctysDenote_tail ts1 (ts2 ++ ts3)
(eq_rect _ ctysDenote x _ Heq)).
Lemma tail_split_pf : forall ts1 ts2 ts3 x,
ctysDenote_tail (ts1 ++ ts2) ts3 x
= ctysDenote_tail _ _
(ctysDenote_tail ts1 (ts2 ++ ts3)
(eq_rect _ ctysDenote x _ (app_ass _ _ _))).
Lemma revApp_ass :forall ts1 ts' ts2 : list cty,
ts1 +++ ts' ++ ts2 = (rev ts1 ++ ts') ++ ts2.
Lemma tail''_tail : forall ts1 ts' ts2 x Heq,
ctysDenote_tail'' ts1 ts' ts2 x =
ctysDenote_tail (rev ts1 ++ ts') ts2
(eq_rect _ ctysDenote x _ Heq).
Lemma tail'_tail : forall ts1 ts2 x Heq,
ctysDenote_tail' ts1 ts2 x =
ctysDenote_tail (rev ts1) ts2
(eq_rect _ ctysDenote x _ Heq).
Lemma tail'_tail_pf : forall ts1 ts2 x,
ctysDenote_tail' ts1 ts2 x =
ctysDenote_tail (rev ts1) ts2
(eq_rect _ ctysDenote x _ (revApp_app _ _)).
Lemma tail'_split : forall a G' G x,
ctysDenote_tail' (a :: G') G x
= ctysDenote_tail' (a :: nil) G (ctysDenote_tail' G' (a :: G) x).
Lemma close'_sound : forall (G ts ftys : list cty) G'
Hsmall (f : cfunc (G ++ CProd (G' +++ G) :: ftys) ts)
x s2 args,
cfuncDenote (close' _ _ Hsmall f) (SCons _ x s2) args
= cfuncDenote f (appSubst (ctysSubst (ctysDenote_tail' _ _ x)) (SCons _ x s2)) args.
Lemma buildEnv'_sound : forall G G' s' s'',
ctysSubst (ts:=G) (cargsDenote (buildEnv' G G') (appSubst s' s''))
= s'.
Lemma close_sound : forall (G ftys : list cty) (ts : ctys) (f : cfunc (G ++ ftys) ts)
s s' G' (s'' : Subst ctyDenote G') args2 Hsmalls,
cfuncDenote (close f Hsmalls) s
(cargsDenote
(buildEnv' _ _)
(appSubst s' s''), args2)
= cfuncDenote f
(appSubst s' s)
args2.
Lemma cargsDenote_app_nil : forall G dom (args : cargs G dom) Heq s,
cargsDenote
(eq_rec _ (fun l : list cty => cargs l dom)
args _ Heq)
(appSubst s (SNil ctyDenote))
= cargsDenote args s.
Theorem buildEnv_apply : forall (G : list cty) (vi : varInfo G) ts s1 s2,
cargsDenote (buildEnv G vi ts) (appSubst s1 s2)
= cargsDenote (buildEnv' (varInfo_apply G vi) ts) (appSubst (Subst_strengthen s1 vi) s2).
Lemma strengthen_app_sound : forall G2 G3 t (e : cfunc (G2 ++ G3) t)
s2 s3,
cfuncDenote (Cfunc.strengthen_app (G1:= nil) e)
(appSubst
(Subst_strengthen s2
(varInfo_take (Cfunc.freeVars e)))
s3) = cfuncDenote e (appSubst s2 s3).
Soundness of the translation |
Scheme oprimop_scheme := Induction for oprimop Sort Prop
with olinear_scheme := Induction for olinear Sort Prop
with ocont_scheme := Induction for ocont Sort Prop
with oargs_scheme := Induction for oargs Sort Prop.
Hint Rewrite VarNil_sound closureVar_sound
splitCtysSubst CprimopDenote.liftEnd'_sound
cargsDenote_app_nil buildEnv_apply
close_sound strengthen_app_sound : CCify.
Ltac my_simpl := (unfold linear_lr, primop_lr, cont_lr, args_lr,
withCont_bind, cprogDenote, cpprogDenote, cfprogDenote, cwithProgDenote in *;
fold ctyDenote in *; fold otyDenote in *; fold vals_lr in *;
fold ccTy in *;
autorewrite with CCify;
try match goal with
| [ |- context[Cfunc.strengthen_app ?B] ] => rewrite (strengthen_app_sound B)
end;
try match goal with
| [ |- context[Clinear.liftMiddle ?fns ?body] ] =>
rewrite (ClinearDenote.liftMiddle_cons_sound (G'':= fns) body)
end;
try match goal with
| [ |- context[ccPrimop ?P] ] => destruct (ccPrimop P)
| [ |- context[ccLinear ?L] ] => destruct (ccLinear L)
| [ |- context[ccCont ?C] ] => destruct (ccCont C)
end).
Ltac my_lr_tac := lr_tac ltac:(var_adder val_lr) stricter_inster my_simpl.
Theorem ccLinear_sound : forall G t (e : olinear G t),
linear_lr e (ccLinear e).