| Closure conversion |
Require Import Arith Eqdep List.
Require Import Max.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Require Import CTPC.AllocMonad.
Require Import CTPC.Dict.
Require Import CTPC.Trace.
Require Import CTPC.Alloc.
Require Import CTPC.Flat.
Set Implicit Arguments.
Tactics |
Hint Rewrite NatDict.sel_empty NatDict.sel_upd_eq : Flatify.
Hint Rewrite NatDict.sel_upd_ne using omega : Flatify.
Ltac simplify := repeat progress (simpl in *; intuition; autorewrite with Flatify;
repeat match goal with
| [ |- context[match ?E with (_, _) => _ end] ] => destruct E; simpl
end).
The flattening translation |
Fixpoint flatVar (G : list aty) (t : aty) (v : Var G t) {struct v} : nat :=
match v with
| First G' _ => length G'
| Next _ _ _ v' => flatVar v'
end.
Theorem flatVar_bound : forall G t (v : Var G t),
flatVar v < length G.
Theorem flatVar_sel : forall G t (v : Var G t),
NatDict.sel (flatContext G) (flatVar v) = t.
Fixpoint flatArgs G ts (args : aargs G ts) {struct args} : fargs (flatContext G) ts :=
match args in (aargs G ts) return (fargs (flatContext G) ts) with
| AANil _ => FANil _
| AACons G' _ ts' v args' =>
eq_rec _ (fun V => fargs (flatContext G') (V :: ts'))
(FACons _ (flatArgs args'))
_ (flatVar_sel v)
end.
Definition flatPrimop G t (op : aprimop G t) : fprimop (flatContext G) t :=
match op in (aprimop G t) return (fprimop (flatContext G) t) with
| AVar G' _ v => eq_rec _ (fprimop (flatContext G')) (FSlot _ _) _ (flatVar_sel v)
| AConst _ n => FConst _ n
| ACodeptr _ _ n => FCodeptr _ _ n
| ANew _ _ args => FNew (flatArgs args)
| AProj _ _ v pos => FProj _ (flatVar_sel v) pos
end.
Fixpoint copyType (tp : ftyping) (to from len : nat) {struct len} : ftyping :=
match len with
| O => tp
| S len' => NatDict.upd (copyType tp (S to) (S from) len') to
(NatDict.sel (copyType tp (S to) (S from) len') from)
end.
Fixpoint copy (tp : ftyping) (to from len : nat) {struct len}
: flinear (copyType tp to from len) -> flinear tp :=
match len return (flinear (copyType tp to from len) -> flinear tp) with
| O => fun lin => lin
| S len' => fun lin => copy _ _ _ _ (FSet (FSlot (copyType _ _ _ _) _) lin)
end.
Fixpoint stashType (tp : ftyping) (start : nat) (ts : list aty) {struct ts} : ftyping :=
match ts with
| nil => tp
| t :: ts' => NatDict.upd (stashType tp (S start) ts') start t
end.
Lemma stashType_early : forall ts tp start sl,
sl < start
-> NatDict.sel tp sl
= NatDict.sel (stashType tp start ts) sl.
Lemma stashType_early' : forall ts tp start sl,
sl < start
-> NatDict.sel tp sl
= NatDict.sel (stashType tp (S start) ts) sl.
Fixpoint args_early (tp : ftyping) (ts : list aty) (args : fargs tp ts) (start : nat) {struct args} : Prop :=
match args with
| FANil _ => True
| FACons _ _ sl args' => sl < start /\ args_early args' start
end.
Theorem early_bump : forall (tp : ftyping) (ts : list aty) (args : fargs tp ts) (start : nat),
args_early args start
-> args_early args (S start).
Implicit Arguments early_bump [tp ts args start].
Fixpoint stash (tp : ftyping) (ts : list aty) (args : fargs tp ts) (start : nat) {struct args}
: args_early args start -> flinear (stashType tp start ts) -> flinear tp :=
match args in (fargs tp ts) return (args_early args start -> flinear (stashType tp start ts) -> flinear tp) with
| FANil _ => fun _ lin => lin
| FACons _ _ sl args' => fun Hearly lin => stash args' _ (early_bump (proj2 Hearly))
(FSet (FSlot _ sl)
(eq_rec _ (fun V => flinear (NatDict.upd _ _ V))
lin
_ (stashType_early' _ _ (proj1 Hearly))))
end.
Fixpoint args_max G ts (args : fargs G ts) {struct args} : nat :=
match args with
| FANil _ => 0
| FACons _ _ sl args' => max sl (args_max args')
end.
Definition args_bound G ts (args : fargs G ts) :=
S (max (length ts) (args_max args)).
Theorem args_early_monotone : forall G ts (args : fargs G ts) n1 n2,
args_early args n1
-> n1 <= n2
-> args_early args n2.
Theorem args_max_early : forall G ts (args : fargs G ts),
args_early args (S (args_max args)).
Theorem args_bound_early : forall G ts (args : fargs G ts),
args_early args (args_bound args).
Theorem stashType_sound : forall (ts : list aty) (tp : ftyping) (start : nat) n t,
nth_error ts n = value t
-> NatDict.sel (stashType tp start ts) (n + start) = t.
Lemma copyType_late : forall len tp to from sl,
sl > to + len
-> NatDict.sel (copyType tp to from len) sl
= NatDict.sel tp sl.
Theorem copyType_sound : forall len tp to from pos,
to + len < from
-> pos < len
-> NatDict.sel (copyType tp to from len) (pos + to)
= NatDict.sel tp (pos + from).
Lemma stashType_late : forall ts tp start sl,
sl >= start + length ts
-> NatDict.sel tp sl
= NatDict.sel (stashType tp start ts) sl.
Theorem flatCall_sel : forall tp bound ts t,
NatDict.sel (copyType
(stashType
(NatDict.upd tp (S bound + length ts) t)
(S bound) ts) 0
(S bound) (length ts)) (S bound + length ts) = t.
Theorem call_precondition : forall G ts
(args : fargs (flatContext G) ts) t,
fprecondition
(copyType
(stashType
(NatDict.upd (flatContext G) (args_bound args + length ts) t)
(args_bound args) ts)
0 (args_bound args) (length ts)) ts.
Lemma upd_early : forall (f : ftyping) a t sl,
sl < a
-> NatDict.sel (NatDict.upd f a t) sl
= NatDict.sel f sl.
Fixpoint frob_args tp ts (args : fargs tp ts) a t {struct args}
: args_early args a -> fargs (NatDict.upd tp a t) ts :=
match args in (fargs tp ts) return (args_early args a -> fargs (NatDict.upd tp a t) ts) with
| FANil _ => fun Hearly => FANil _
| FACons _ _ sl args' => fun Hearly =>
eq_rec _ (fun V => fargs _ (V :: _))
(FACons sl (frob_args args' a t (proj2 Hearly)))
_ (upd_early _ _ (proj1 Hearly))
end.
Theorem frob_args_early : forall tp ts (args : fargs tp ts) bound,
args_early args bound
-> forall a t Hearly, args_early (frob_args args a t Hearly) bound.
Theorem flatCall_lemma : forall G ts (args : fargs (flatContext G) ts),
args_early args (args_bound args + length ts).
Definition flatCall : forall G ts
(args : fargs (flatContext G) ts) t,
flinear
(copyType
(stashType
(NatDict.upd (flatContext G) (args_bound args + length ts) t)
(args_bound args) ts)
0 (args_bound args) (length ts))
-> flinear (NatDict.upd (flatContext G) (args_bound args + length ts) t).
Fixpoint flatLinear G t (lin : alinear G t) {struct lin} : flinear (flatContext G) :=
match lin in (alinear G t) return (flinear (flatContext G)) with
| AApply bip moop f args =>
FSet (FSlot _ (flatVar f))
(eq_rec _ (fun T => flinear (NatDict.upd _ _ T))
(flatCall _ (flatArgs args) _ (FJump (flatCall_sel _ _ _ _) (call_precondition _ (flatArgs args) _)))
_ (sym_eq (flatVar_sel _)))
| ABind _ _ op lin' => FSet (flatPrimop op) (flatLinear lin')
end.
Fixpoint afuncBody G ts (f : afunc G ts) {struct f} : alinear (ts +++ G) tt :=
match f in (afunc G ts) return (alinear (ts +++ G) tt) with
| AFBody _ lin => lin
| AFLam _ _ _ f' => afuncBody f'
end.
Definition flatFunc G ts (f : afunc G ts) : flinear (flatContext (ts +++ G)) :=
flatLinear (afuncBody f).
Definition flatProg (G : list aty) (pr : aprog G) : fprog (flatContext G) :=
Build_fprog
(map (fun ts => flatContext (ts +++ nil)) (aFuncTys pr))
(mapI (f:= fun ts => flatContext (ts +++ nil))
(flatFunc (G:= nil)) (aFuncs pr))
(flatLinear (aBody pr)).
Logical relations |
Section slots_Subst.
Variable sls : slots.
Fixpoint slots_Subst (G : list aty) (s : Subst atyDenote G) {struct s} : Prop :=
match s with
| SNil => True
| SCons t G' v s' => v = NatDict.sel sls (length G') /\ slots_Subst s'
end.
Definition slots_args (args : list adom) :=
forall n tg v, nth_error args n = value (tg, v)
-> NatDict.sel sls n = v.
Fixpoint slots_actuals (n : nat) (ts : atys) {struct ts} : aformalsDenote ts-> Prop :=
match ts return (aformalsDenote ts-> Prop) with
| nil => fun _ => True
| t :: ts' => fun args =>
NatDict.sel sls n = fst args
/\ slots_actuals (S n) ts' (snd args)
end.
End slots_Subst.
Definition val_lr (t : aty) (v1 v2 : atyDenote t) := v1 = v2.
Definition args_lr G ts (args1 : aargs G ts) (args2 : fargs (flatContext G) ts) :=
forall sls s, slots_Subst sls s
-> aargsDenote args1 s
= fargsDenote args2 sls.
Definition primop_lr G t (op1 : aprimop G t) (op2 : fprimop (flatContext G) t) :=
forall sls s, slots_Subst sls s
-> aprimopDenote op1 s
= fprimopDenote op2 sls.
Definition linear_lr G t (lin1 : alinear G t) (lin2 : flinear (flatContext G)) :=
forall sls s, slots_Subst sls s
-> forall st,
match alinearDenote lin1 s st with
| None =>
match flinearDenote lin2 sls st with
| None => True
| Some _ => False
end
| Some (st', (pc, argsT, args)) =>
exists sls',
flinearDenote lin2 sls st = Some (st', (pc, argsT, sls'))
/\ slots_args sls' args
end.
Definition prog_lr G (pr1 : aprog G) (pr2 : fprog (flatContext G)) :=
forall sls s, slots_Subst sls s
-> forall st output,
runTrace (aprogDenote pr1 s st) output
-> runTrace (fprogDenote pr2 sls st) output.
Tactics |
Ltac my_simpl := repeat progress
(unfold args_lr, primop_lr, linear_lr, prog_lr in *;
autorewrite with Flatify;
repeat inversion_Subst_any; subst).
Ltac my_inster T k := fail.
Ltac my_lr_tac := lr_tac ltac:(var_adder val_lr) my_inster my_simpl.
Soundness proofs |
Lemma slots_Subst_sound : forall G t (v : Var G t) sls s,
slots_Subst sls s
-> VarDenote v s = NatDict.sel sls (flatVar v).
Hint Resolve flatVar_sel.
Hint Extern 1 (_ = _) =>
match goal with
| [ H : slots_Subst _ _ |- context[VarDenote ?V _] ] =>
rewrite (slots_Subst_sound V _ _ H)
end.
Theorem flatArgs_sound : forall G ts (args : aargs G ts),
args_lr args (flatArgs args).
Hint Extern 1 (_ = _) =>
match goal with
| [ H : slots_Subst _ _, args : aargs _ _ |- _ ] =>
rewrite (flatArgs_sound args _ _ H)
end.
Theorem flatPrimop_sound : forall G t (op : aprimop G t),
primop_lr op (flatPrimop op).
Lemma slots_Subst_upd : forall sls a n G (s : Subst atyDenote G),
slots_Subst sls s
-> a >= length G
-> slots_Subst (NatDict.upd sls a n) s.
Hint Resolve slots_Subst_upd.
Fixpoint copySlots (sls : slots) (to from len : nat) {struct len} : slots :=
match len with
| O => sls
| S len' => NatDict.upd (copySlots sls (S to) (S from) len') to
(NatDict.sel (copySlots sls (S to) (S from) len') from)
end.
Fixpoint stashSlots (sls : slots) (start : nat) (args : list adom) {struct args} : slots :=
match args with
| nil => sls
| (_, v) :: args' => NatDict.upd (stashSlots sls (S start) args') start v
end.
Hint Resolve stashType_early'.
Lemma stashSlots_early : forall ts sls start sl,
sl < start
-> NatDict.sel (stashSlots sls start ts) sl
= NatDict.sel sls sl.
Theorem stash_soundness : forall (tp : ftyping) (ts : list aty) (args : fargs tp ts) (start : nat)
(Hearly : args_early args start)
(lin : flinear (stashType tp start ts)) sls,
flinearDenote (stash args start Hearly lin) sls
= flinearDenote lin (stashSlots sls start (fargsDenote args sls)).
Theorem copy_soundness : forall (len : nat) (tp : ftyping) (to from : nat)
(lin : flinear (copyType tp to from len)) sls,
flinearDenote (copy tp to from len lin) sls
= flinearDenote lin (copySlots sls to from len).
Lemma copySlots_late : forall len tp to from sl,
sl > to + len
-> NatDict.sel (copySlots tp to from len) sl
= NatDict.sel tp sl.
Lemma stashSlots_late : forall args sls start sl,
sl >= start + length args
-> NatDict.sel (stashSlots sls start args) sl
= NatDict.sel sls sl.
Lemma fargsDenote_len : forall G ctx (e : fargs G ctx) (sls : slots),
length (fargsDenote e sls) = length ctx.
Lemma aargsDenote_len : forall G ctx (e : aargs G ctx) s,
length (aargsDenote e s) = length ctx.
Theorem copySlots_sound : forall len tp to from pos,
to + len < from
-> pos < len
-> NatDict.sel (copySlots tp to from len) (pos + to)
= NatDict.sel tp (pos + from).
Theorem stashSlots_sound : forall args sls (start : nat) n tg v,
nth_error args n = value (tg, v)
-> NatDict.sel (stashSlots sls start args) (n + start) = v.
Theorem frob_args_sound : forall tp ts (args : fargs tp ts) a t
(Hearly : args_early args a) sls v,
fargsDenote (frob_args args a t Hearly) (NatDict.upd sls a v)
= fargsDenote args sls.
Theorem flatLinear_sound : forall G t (lin : alinear G t),
linear_lr lin (flatLinear lin).
Theorem slots_args_app : forall sls args2 args1,
slots_args sls (args1 ++ rev args2)
-> slots_args sls args1.
Theorem slots_args_app1 : forall sls arg args1,
slots_args sls (args1 ++ arg :: nil)
-> slots_args sls args1.
Hint Resolve slots_args_app1.
Fixpoint augmentSubst ts G (s : Subst atyDenote G) {struct ts}
: aformalsDenote ts -> Subst atyDenote (ts +++ G) :=
match ts return (aformalsDenote ts -> Subst atyDenote (ts +++ G)) with
| nil => fun _ => s
| _ :: _ => fun args => augmentSubst _ (SCons _ (fst args) s) (snd args)
end.
Implicit Arguments augmentSubst [ts G].
Lemma afuncBody_sound : forall G ts (f : afunc G ts) s args,
afuncDenote f s args
= alinearDenote (afuncBody f) (augmentSubst s args).
Section slots_Subst'.
Variable sls : slots.
Variable offset : nat.
Fixpoint slots_Subst' (G : list aty) (s : Subst atyDenote G) {struct s} : Prop :=
match s with
| SNil => True
| SCons t G' v s' => v = NatDict.sel sls (offset + length G') /\ slots_Subst' s'
end.
Definition slots_args' (args : list adom) :=
forall n tg v, nth_error args n = value (tg, v)
-> NatDict.sel sls (offset + n) = v.
End slots_Subst'.
Lemma slots_Subst_func : forall ts sls args G,
slots_args' sls (length G) args
-> forall (s : Subst atyDenote G),
slots_Subst sls s
-> forall Heq, slots_Subst sls
(augmentSubst s (makeActuals ts args Heq)).
Lemma flatProg_sound' : forall tr output, runTrace tr output
-> forall G (pr : aprog G) sls st pc argsT args,
tr = amakeTrace pr st pc argsT args
-> slots_args sls args
-> runTrace (fmakeTrace (flatProg pr) st pc argsT sls) output.
Theorem flatProg_sound : forall G (pr : aprog G),
prog_lr pr (flatProg pr).