| Combined code flattening and allocation explicitation |
Require Import Arith Bool Eqdep List TheoryList.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.LambdaTamer.
Require Import LambdaTamer.Tactics.
Require Import CTPC.Continuation.
Require Import CTPC.CC.
Require Import CTPC.AllocMonad.
Require Import CTPC.Trace.
Require Import CTPC.Alloc.
Set Implicit Arguments.
Generic syntactic functions and their soundness proofs |
Definition insert t G (lin : alinear (t :: G) tt) t' : alinear (t :: t' :: G) tt :=
Alinear.lift' (t :: nil) G lin t'.
Lemma insert_sound : forall G t t' (lin : alinear (t :: G) tt)
(s : Subst atyDenote G)
(x : atyDenote t') (x0 : atyDenote t),
alinearDenote (insert lin t') (SCons t x0 (SCons t' x s)) =
alinearDenote lin (SCons t x0 s).
Implicit Arguments insert [t G].
Hint Resolve AlinearDenote.lift_sound insert_sound.
Auxiliary syntactic types |
Inductive aprimopB : list aty -> aty -> Set :=
| AFinal : forall G t,
aprimop G t
-> aprimopB G t
| ABindB : forall G t' t,
aprimop G t'
-> aprimopB (t' :: G) t
-> aprimopB G t.
Fixpoint aprimopBDenote (G : list aty) (t : aty) (opB : aprimopB G t) {struct opB}
: Subst atyDenote G -> aprimopTy t :=
match opB in (aprimopB G t) return (Subst atyDenote G -> aprimopTy t) with
| AFinal _ _ op => aprimopDenote op
| ABindB _ _ _ op opB' => fun s =>
v <- aprimopDenote op s;
aprimopBDenote opB' (SCons _ v s)
end.
Fixpoint splice (G : list aty) (t : aty) (opB : aprimopB G t) {struct opB}
: alinear (t :: G) tt -> alinear G tt :=
match opB in (aprimopB G t) return (alinear (t :: G) tt -> alinear G tt) with
| AFinal _ _ op => ABind op
| ABindB _ _ _ op opB' => fun lin => ABind op (splice opB' (insert lin _))
end.
Theorem splice_sound : forall (G : list aty) (t : aty) (opB : aprimopB G t)
(lin : alinear (t :: G) tt) s st P,
allocSpec st
(v <- aprimopBDenote opB s;
alinearDenote lin (SCons _ v s)) P
-> allocSpec st (alinearDenote (splice opB lin) s) P.
A nested-type-friendly induction principle for ctys |
Section Induction.
Variable P : cty -> Prop.
Variable P' : ctys -> Prop.
Hypothesis P_Nat : P CNat.
Hypothesis P_Cont : forall ts, P' ts -> P (CCont ts).
Hypothesis P_Prod : forall ts, P' ts -> P (CProd ts).
Hypothesis P_Code : forall ctx ts, P' ctx -> P' ts -> P (CCode ctx ts).
Hypothesis P'_nil : P' nil.
Hypothesis P'_cons : forall t ts, P t -> P' ts -> P' (t :: ts).
Fixpoint cty_ind' (t : cty) : P t :=
match t return (P t) with
| CNat => P_Nat
| CCont ts =>
P_Cont ((fix ctys_ind' (ts : ctys) : P' ts :=
match ts return (P' ts) with
| nil => P'_nil
| t :: ts' => P'_cons (cty_ind' t) (ctys_ind' ts')
end) ts)
| CProd ts =>
P_Prod ((fix ctys_ind' (ts : ctys) : P' ts :=
match ts return (P' ts) with
| nil => P'_nil
| t :: ts' => P'_cons (cty_ind' t) (ctys_ind' ts')
end) ts)
| CCode ctx ts =>
P_Code ((fix ctys_ind' (ts : ctys) : P' ts :=
match ts return (P' ts) with
| nil => P'_nil
| t :: ts' => P'_cons (cty_ind' t) (ctys_ind' ts')
end) ctx)
((fix ctys_ind' (ts : ctys) : P' ts :=
match ts return (P' ts) with
| nil => P'_nil
| t :: ts' => P'_cons (cty_ind' t) (ctys_ind' ts')
end) ts)
end.
End Induction.
Type translation |
Fixpoint allocTy (t : cty) : aty :=
match t with
| CNat => ANat
| CCont _ => ARef
| CProd _ => ARef
| CCode _ args =>
ACode (ARef :: (fix allocTys (ts : ctys) : atys :=
match ts with
| nil => nil
| t :: ts' => allocTy t :: allocTys ts'
end) args)
end.
Fixpoint allocTys (ts : ctys) : atys :=
match ts with
| nil => nil
| t :: ts' => allocTy t :: allocTys ts'
end.
Term translation |
Fixpoint isLarges' (ts : ctys) : bool :=
match ts with
| nil => true
| t :: s => negb (isSmall' t) && isLarges' s
end.
Definition isLarges ts := isLarges' ts = true.
Theorem negb_true_intro : forall b,
b = false
-> negb b = true.
Theorem negb_prop : forall b,
negb b = true
-> b = false.
Ltac bool_simpl :=
repeat (match goal with
| [ H : _ |- _ ] =>
(generalize (andb_prop _ _ H)
|| generalize (orb_prop _ _ H)
|| generalize (negb_prop _ H));
clear H; intro H
end
|| apply andb_true_intro
|| apply orb_true_intro
|| apply negb_true_intro).
Ltac simplify := repeat progress (simpl in *; intuition; bool_simpl).
Definition allocVar' : forall (G fns : list cty) (t : cty) (x : Var (G ++ fns) t),
isLarges fns -> isSmall t -> Var G t.
Definition allocVar : forall (G : list cty) (t : cty) (x : Var G t),
forall G' fns, G = G' ++ fns
-> isLarges fns -> isSmall t -> Var G' t.
Definition allocArgs (G : list cty) (ts : ctys) (args : cargs G ts)
: isSmalls ts
-> forall G' fns, G = G' ++ fns -> isLarges fns
-> aargs (map allocTy G') (allocTys ts).
Fixpoint allocProj (G : list cty) (pt : cprojTy) (p : cproj G pt) {struct p}
: nat :=
match p with
| CPFst _ _ _ => O
| CPSnd _ _ _ _ p' => S (allocProj p')
end.
Lemma isSmall'_obvious : forall t : smallCty,
isSmall' (proj1_sig t) = true.
Hint Resolve isSmall'_obvious.
Lemma isSmall_obvious : forall t : smallCty,
isSmall (proj1_sig t).
Hint Resolve isSmall_obvious.
Lemma isSmalls_obvious : forall ctx : smallCtys,
isSmalls (proj1_sig ctx).
Hint Resolve isSmalls_obvious.
Lemma isSmalls_nil : isSmalls nil.
Hint Resolve isSmalls_nil.
Hint Unfold isSmall.
Section allocCode.
Variable allocCode : forall (G : list cty) (t : cty) (x : Var G t), nat.
Definition allocPrimop (G : list cty) (t : cty) (op : cprimop G t)
: forall G' fns, G = G' ++ fns
-> isLarges fns
-> aprimopB (map allocTy G') (allocTy t).
Definition allocLinear (G : list cty) (t : unit) (lin : clinear G t)
: forall G' fns, G = G' ++ fns
-> isLarges fns
-> alinear (map allocTy G') tt.
End allocCode.
Fixpoint allocCode (G : list cty) (t : cty) (x : Var G t) {struct x} : nat :=
match x with
| First G _ => length G
| Next _ _ _ x' => allocCode x'
end.
Definition allocFunc (G : list cty) (ts : ctys) (f : cfunc G ts)
: forall G' fns, G = G' ++ fns
-> isLarges fns
-> afunc (map allocTy G') (allocTys ts).
Definition getLarge (t : cty) (Ht : ~isSmall t) : ctys.
Definition allocFuncTys (ts : ctys)
: isLarges ts -> list atys.
Definition allocFuncs (G : list cty) (ts : ctys) (fs : cfuncs G ts)
: isLarges G
-> forall (Hts : isLarges ts),
listI (afunc nil) (allocFuncTys Hts).
Lemma cfuncs_larges : forall (G : list cty) (ts : ctys) (fs : cfuncs G ts),
isLarges ts.
Definition allocProg (G : list cty) (p : cprog G tt) : aprog (map allocTy G) :=
Build_aprog
(allocFuncTys (cfuncs_larges (cDefs p)))
(allocFuncs (cDefs p) (refl_equal _) (cfuncs_larges (cDefs p)))
(allocLinear (fun _ _ x => length (cFns p) - S (allocCode x)) (cBody p) G (refl_equal _) (cfuncs_larges (cDefs p))).
Logical relations |
Section Traces.
Variable Gpr : list cty.
Variable pr : cprog Gpr tt.
Fixpoint val_lr (st : mem adom) (t : cty) {struct t} : ctyDenote t -> atyDenote (allocTy t) -> Prop :=
match t return (ctyDenote t -> atyDenote (allocTy t) -> Prop) with
| CNat => fun n1 n2 => n1 = n2
| CProd ts => fun recd base =>
match nth_error st base with
| error => False
| value fds =>
(fix vals_lr (st : mem adom) (ts : ctys) {struct ts} : ctysDenote ts -> list adom -> Prop :=
match ts return (ctysDenote ts -> list adom -> Prop) with
| nil => fun _ fds =>
match fds with
| nil => True
| _ => False
end
| t :: ts' => fun recd fds =>
match fds with
| nil => False
| (tg, v2) :: fds' => tg = tagof (allocTy t) /\ val_lr st t (fst recd) v2 /\ vals_lr st ts' (snd recd) fds'
end
end) st ts recd fds
end
| CCode ctx args => fun f1 f2 =>
forall st' env1 args1 env2 args2,
match nth_error (st ++ st') env2 with
| error => False
| value fds =>
(fix vals_lr (st : mem adom) (ts : ctys) {struct ts} : ctysDenote ts -> list adom -> Prop :=
match ts return (ctysDenote ts -> list adom -> Prop) with
| nil => fun _ fds =>
match fds with
| nil => True
| _ => False
end
| t :: ts' => fun recd fds =>
match fds with
| nil => False
| (tg, v2) :: fds' => tg = tagof (allocTy t) /\ val_lr st t (fst recd) v2 /\ vals_lr st ts' (snd recd) fds'
end
end) (st ++ st') ctx env1 fds
/\ (fix vals_lr (st : mem adom) (ts : ctys) {struct ts} : ctysDenote ts -> list adom -> Prop :=
match ts return (ctysDenote ts -> list adom -> Prop) with
| nil => fun args1 args2 =>
match args2 with
| nil => True
| _ => False
end
| t :: ts' => fun args1 args2 =>
match args2 with
| nil => False
| (tg, arg2) :: args2' => tg = tagof (allocTy t) /\ val_lr st t (fst args1) arg2 /\ vals_lr st ts' (snd args1) args2'
end
end) (st ++ st') args args1 args2
end
-> runTrace (amakeTrace (allocProg pr) (st ++ st') f2 (ARef :: map allocTy args) ((Traced, env2) :: args2))
(f1 (env1, args1))
| CCont args => fun f1 closure =>
match nth_error st closure with
| value ((Untraced, f2) :: (Traced, env2) :: nil) =>
forall st' args1 args2,
(fix vals_lr (st : mem adom) (ts : ctys) {struct ts} : ctysDenote ts -> list adom -> Prop :=
match ts return (ctysDenote ts -> list adom -> Prop) with
| nil => fun args1 args2 =>
match args2 with
| nil => True
| _ => False
end
| t :: ts' => fun args1 args2 =>
match args2 with
| nil => False
| (tg, arg2) :: args2' => tg = tagof (allocTy t) /\ val_lr st t (fst args1) arg2 /\ vals_lr st ts' (snd args1) args2'
end
end) (st ++ st') args args1 args2
-> runTrace (amakeTrace (allocProg pr) (st ++ st') f2 (ARef :: map allocTy args) ((Traced, env2) :: args2))
(f1 args1)
| _ => False
end
end.
Fixpoint vals_lr (st : mem adom) (ts : ctys) {struct ts} : ctysDenote ts -> list adom -> Prop :=
match ts return (ctysDenote ts -> list adom -> Prop) with
| nil => fun args1 args2 =>
match args2 with
| nil => True
| _ => False
end
| t :: ts' => fun args1 args2 =>
match args2 with
| nil => False
| (tg, arg2) :: args2' => tg = tagof (allocTy t) /\ val_lr st t (fst args1) arg2 /\ vals_lr st ts' (snd args1) args2'
end
end.
Hint Constructors Subst_lr.
Definition Subst_lr st := Subst_lr allocTy (val_lr st).
Hint Unfold Subst_lr.
The soundness proofs |
Theorem allocVar'_sound : forall (G fns : list cty) (t : cty) (x : Var (G ++ fns) t)
(Hfns : isLarges fns) (Ht : isSmall t) (s1 : Subst ctyDenote G) s1',
VarDenote (allocVar' _ x Hfns Ht) s1
= VarDenote x (appSubst s1 s1').
Theorem allocVar_sound : forall (G : list cty) (t : cty) (x : Var G t)
G' fns (Heq : G = G' ++ fns)
(Hfns : isLarges fns) (Ht : isSmall t) (s1 : Subst ctyDenote G') s1',
VarDenote (allocVar x _ Heq Hfns Ht) s1
= VarDenote x (eq_rect _ (Subst ctyDenote) (appSubst s1 s1') _ (sym_eq Heq)).
Theorem allocProj_sound : forall (G : list cty) (pt : cprojTy) (p : cproj G pt) st s fs1 fs2,
vals_lr st _ fs1 fs2
-> match nth_error fs2 (allocProj p) with
| error => False
| value (tg, v2) => tg = tagof (allocTy (ctChosen pt)) /\ val_lr st _ (cprojDenote p s fs1) v2
end.
Hint Rewrite nth_error_grab nth_error_grab' nth_error_grab_last : Allocify.
Ltac my_var_adder :=
repeat match goal with
| [ H : Subst_lr _ _ _ |- context[allocVar ?X ?G' ?Heq ?Hfns ?Ht] ] =>
match goal with
| [ H' : val_lr _ _ (VarDenote (allocVar X G' Heq Hfns Ht) _) _ |- _ ] => fail 1
| _ => generalize (Subst_lr_Var (allocVar X G' Heq Hfns Ht) H); intro
end
end.
Ltac caseEq e := generalize (refl_equal e); pattern e at -1; case e.
Ltac elim_match :=
match goal with
| [ H : match ?E with Some _ => _ | None => False end |- _ ] =>
let v := fresh "v" with Hv := fresh "Hv" in
(caseEq E; [intros v Hv; rewrite Hv in H
| intro Hv; rewrite Hv in H; tauto])
| [ H : match ?E with _ :: _ => _ | nil => False end |- _ ] =>
let hd := fresh "hd" with tl := fresh "tl" with Hls := fresh "Hls" in
(caseEq E; [intro Hls; rewrite Hls in H; tauto
| intros hd tl Hls; rewrite Hls in H])
| [ H : match ?E with _ :: _ => False | nil => _ end |- _ ] =>
let hd := fresh "hd" with tl := fresh "tl" with Hls := fresh "Hls" in
(caseEq E; [intro Hls; rewrite Hls in H
| intros hd tl Hls; rewrite Hls in H; tauto])
| [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst
| [ H : context[match ?E with (_, _) => _ end] |- _ ] =>
destruct E; simpl in *
| [ H : context[match ?E with Traced => _ | Untraced => _ end] |- _ ] =>
destruct E; simpl in *
end.
Hint Rewrite app_ass : Allocify.
Ltac my_rewriter :=
repeat match goal with
| [ H : context[allocVar ?V _ ?PF ?Hfns ?Ht], s1 : Subst _ _, s1' : Subst _ _ |- _ ] =>
rewrite (allocVar_sound V PF Hfns Ht s1 s1') in H
| [ H : nth_error _ _ = Some ?x |- _ ] => rewrite (nth_error_monotone (x:= x)); trivial
| [ H : _ |- _ ] => rewrite app_ass in H
end;
autorewrite with Allocify.
Ltac my_simpl := repeat progress (unfold withCont_bind, checkTag in *; fold vals_lr in *;
repeat elim_match;
try match goal with
| [ c : cproj _ _ , s1 : Subst _ _, s1' : Subst _ _, H0 : _ |- _ ] =>
generalize (allocProj_sound c _ (appSubst s1 s1') _ _ H0); clear H0
end;
allocM_solver;
try apply splice_sound).
Ltac my_inster T k :=
match T with
| mem _ => fail 1
| list (list adom) => fail 1
| list cty => fail 1
| _ => default_inster T k
end.
Ltac my_lr_tac := lr_tac my_var_adder my_inster ltac:(my_simpl; my_rewriter).
Theorem val_lr_monotone : forall t st v1 v2,
val_lr st t v1 v2
-> forall st', val_lr (st ++ st') t v1 v2.
Hint Resolve val_lr_monotone.
Theorem vals_lr_monotone : forall ts st vs1 vs2,
vals_lr st ts vs1 vs2
-> forall st', vals_lr (st ++ st') ts vs1 vs2.
Hint Resolve vals_lr_monotone.
Theorem Subst_lr_monotone : forall st G (s1 : Subst ctyDenote G) s2,
Subst_lr st s1 s2
-> forall st', Subst_lr (st ++ st') s1 s2.
Hint Resolve Subst_lr_monotone.
Theorem allocVar_sound_lr : forall G' fns t st s1 s1' s2,
Subst_lr st s1 s2
-> forall (v : Var (G' ++ fns) t) Heq Hfns Ht,
val_lr st t (VarDenote v (appSubst s1 s1'))
(VarDenote
(VarConvert allocTy
(allocVar v G' (fns:= fns) Heq Hfns Ht))
s2).
Hint Resolve allocVar_sound_lr.
Theorem allocArgs_sound : forall G ts (args : cargs G ts)
(Hts : isSmalls ts)
G' fns (Heq : G = G' ++ fns)
(Hfns : isLarges fns)
s1 s1' s2 st, Subst_lr st s1 s2
-> vals_lr st ts
(cargsDenote args (eq_rect _ (Subst ctyDenote) (appSubst s1 s1') _ (sym_eq Heq)))
(aargsDenote (allocArgs args Hts _ Heq Hfns) s2).
Hint Resolve allocArgs_sound.
Section allocCode_soundness.
Variable allocCode : forall (G : list cty) (t : cty) (x : Var G t), nat.
Variable fns : list cty.
Variable s1' : Subst ctyDenote fns.
Definition allocCode_soundness := forall st (ctx : smallCtys) args G'
(s1 : Subst ctyDenote G')
(v : Var (G' ++ fns) (CCode (proj1_sig ctx) args))
env1 (args1 : ctysDenote args) env2 (args2 : list adom),
isSmalls G'
-> val_lr st (CProd (proj1_sig ctx)) env1 env2
-> vals_lr st args args1 args2
-> runTrace
(amakeTrace (allocProg pr) st (S (allocCode v)) (ARef :: allocTys args) ((Traced, env2) :: args2))
(VarDenote v (appSubst s1 s1') (env1, args1)).
End allocCode_soundness.
Section allocCode.
Definition primop_lr G fns t (op1 : cprimop (G ++ fns) t) (op2 : aprimop (map allocTy G) (allocTy t)) :=
forall st s1 s1' s2, Subst_lr st s1 s2
-> allocSpec st (aprimopDenote op2 s2)
(fun st' v2 =>
val_lr st' t (cprimopDenote op1 (appSubst s1 s1')) v2).
Variable allocCode : forall (G : list cty) (t : cty) (x : Var G t), nat.
Variable fns : list cty.
Variable s1' : Subst ctyDenote fns.
Hypothesis allocCode_sound : forall st (ctx : smallCtys) args G'
(s1 : Subst ctyDenote G')
(v : Var (G' ++ fns) (CCode (proj1_sig ctx) args))
env1 (args1 : ctysDenote args) env2 (args2 : list adom),
isSmalls G'
-> val_lr st (CProd (proj1_sig ctx)) env1 env2
-> vals_lr st args args1 args2
-> runTrace
(amakeTrace (allocProg pr) st (S (allocCode v)) (ARef :: allocTys args) ((Traced, env2) :: args2))
(VarDenote v (appSubst s1 s1') (env1, args1)).
Lemma mem_nil_end : forall (st : mem adom),
st = st ++ nil.
Hint Resolve mem_nil_end.
Theorem allocPrimop_sound : forall (G : list cty) (t : cty) (op : cprimop G t)
G' (Heq : G = G' ++ fns)
(Hfns : isLarges fns) st s1 s2,
isSmalls G'
-> Subst_lr st s1 s2
-> allocSpec st
(aprimopBDenote (allocPrimop allocCode op _ Heq Hfns) s2)
(fun st' v2 => val_lr st' t
(cprimopDenote op (eq_rect _ (Subst ctyDenote) (appSubst s1 s1') _ (sym_eq Heq))) v2
/\ exists st'', st' = st ++ st'').
Hint Extern 1 (allocSpec _ (aprimopBDenote (allocPrimop _ ?op ?G' ?Heq ?Hfns) _) _) =>
match goal with
| [ H0 : isSmalls _, H : Subst_lr _ _ _ |- _ ] =>
apply (allocPrimop_sound op Heq Hfns H0 H)
end.
Hint Rewrite AargsDenote.lift_sound : Allocify.
Lemma Subst_lr_fold : forall st G (s1 : Subst ctyDenote G) s2,
Subst_lr st s1 s2
-> Binding.Subst_lr allocTy (val_lr st) s1 s2.
Hint Resolve Subst_lr_fold.
Theorem allocLinear_sound : forall (G : list cty) (t : unit) (lin : clinear G t)
G' (Heq : G = G' ++ fns)
(Hfns : isLarges fns) st s1 s2,
isSmalls G'
-> Subst_lr st s1 s2
-> allocSpec st
(alinearDenote (allocLinear allocCode lin _ Heq Hfns) s2)
(fun st' v2 =>
runTrace
(amakeTrace (allocProg pr) st' (fst (fst v2)) (snd (fst v2)) (snd v2))
(clinearDenote lin (eq_rect _ (Subst ctyDenote) (appSubst s1 s1') _ (sym_eq Heq)))).
End allocCode.
Section allocFunc_sound.
Variable fns : list cty.
Variable s1' : Subst ctyDenote fns.
Hypothesis allocCode_sound : forall st (ctx : smallCtys) args G'
(s1 : Subst ctyDenote G')
(v : Var (G' ++ fns) (CCode (proj1_sig ctx) args))
env1 (args1 : ctysDenote args) env2 (args2 : list adom),
isSmalls G'
-> val_lr st (CProd (proj1_sig ctx)) env1 env2
-> vals_lr st args args1 args2
-> runTrace
(amakeTrace (allocProg pr) st (S (allocCode v)) (ARef :: allocTys args) ((Traced, env2) :: args2))
(VarDenote v (appSubst s1 s1') (env1, args1)).
Fixpoint args_lr (st : mem adom) (ts : ctys) {struct ts} : ctysDenote ts -> aformalsDenote (map allocTy ts) -> Prop :=
match ts return (ctysDenote ts -> aformalsDenote (map allocTy ts) -> Prop) with
| nil => fun args1 args2 => True
| t :: ts' => fun args1 args2 =>
val_lr st t (fst args1) (fst args2) /\ args_lr st ts' (snd args1) (snd args2)
end.
Definition func_lr (G : list cty) (ts : ctys) (f : cfunc (G ++ fns) ts) (af : afunc (map allocTy G) (map allocTy ts)) :=
forall args1 args2 st s1 s2,
Subst_lr st s1 s2
-> args_lr st _ args1 args2
-> allocSpec st
(afuncDenote af s2 args2)
(fun st' v2 =>
runTrace
(amakeTrace (allocProg pr) st' (fst (fst v2)) (snd (fst v2)) (snd v2))
(cfuncDenote f (appSubst s1 s1') args1)).
Theorem allocFunc_sound : forall (G : list cty) (ts : ctys) (f : cfunc G ts)
G' (Heq : G = G' ++ fns)
(Hfns : isLarges fns),
isSmalls G'
-> func_lr _ (eq_rec _ (fun G => cfunc G ts) f _ Heq) (allocFunc f _ Heq Hfns).
End allocFunc_sound.
Fixpoint funcs_lr (G : list cty) (ts : ctys) (fs : cfuncs G ts) {struct fs}
: forall (Hts : isLarges ts), listI (afunc nil) (allocFuncTys Hts) -> Prop :=
match fs in (cfuncs G ts) return (forall (Hts : isLarges ts), listI (afunc nil) (allocFuncTys Hts) -> Prop) with
| CFNil _ => fun _ _ => True
| CFCons _ _ _ _ f fs' => fun Hts afs =>
(forall s1', allocCode_soundness allocCode s1' -> func_lr s1' nil f (headI afs))
/\ funcs_lr fs' _ (tailI afs)
end.
Theorem allocFuncs_sound : forall (G : list cty) (ts : ctys) (fs : cfuncs G ts)
(HG : isLarges G) (Hts : isLarges ts),
funcs_lr fs _ (allocFuncs fs HG Hts).
Definition prog_lr (G : list cty) (p1 : cprog G tt) (p2 : aprog (map allocTy G)) :=
forall st s1 s2, Subst_lr st s1 s2
-> runTrace (aprogDenote p2 s2 st) (cprogDenote p1 s1).
Fixpoint nthFuncs (G : list cty) (ts : ctys) (fs : cfuncs G ts) (n : nat) {struct fs}
: option (sigS (fun G => sigS (cfunc G))) :=
match fs in (cfuncs G ts) return (option (sigS (fun G => sigS (cfunc G)))) with
| CFNil _ => None
| CFCons _ _ _ _ f fs' =>
match n with
| O => Some (existS (fun G => sigS (cfunc G)) _ (existS _ _ f))
| S n' => nthFuncs fs' n'
end
end.
Theorem nthFuncs_larges : forall G ts (fs : cfuncs G ts) pc G' ts' f,
isLarges G
-> nthFuncs fs pc = Some (existS (fun G => sigS (cfunc G)) G' (existS _ ts' f))
-> isLarges G'.
Lemma allocCode_bound : forall G t (v : Var G t),
allocCode v < length G.
Lemma allocCode_nth : forall G fns (defs : cfuncs G fns) n,
n < length fns
-> exists sg,
nthFuncs defs n = Some sg.
Lemma allocCode_nth_ts' : forall G fns (defs : cfuncs G fns)
ctx args (v : Var fns (CCode ctx args)),
exists pos, exists f,
nthFuncs defs (length fns - S (allocCode v))
= Some (existS (fun G => sigS (cfunc G)) (revAppN fns pos G)
(existS _ (CProd ctx :: args) f)).
Lemma allocCode_nth_ts : forall G fns (defs : cfuncs G fns)
ctx args G' (v : Var (G' ++ fns) (CCode ctx args)),
isSmalls G'
-> exists pos, exists f,
nthFuncs defs (length fns - S (allocCode v))
= Some (existS (fun G => sigS (cfunc G)) (revAppN fns pos G)
(existS _ (CProd ctx :: args) f)).
Theorem internal_nthI : forall G ts (fs : cfuncs G ts) pc G' ts' f
(HG : isLarges G)
(Hnth : nthFuncs fs pc = Some (existS (fun G => sigS (cfunc G)) G' (existS _ ts' f))),
nthI (allocFuncs fs HG (cfuncs_larges fs)) pc
= Some (existS (afunc nil) (allocTys ts')
(allocFunc f nil (refl_equal _) (nthFuncs_larges fs pc HG Hnth))).
Lemma length_allocTys : forall ts,
length (allocTys ts) = length ts.
Lemma length_args : forall st args (args1 : ctysDenote args) args2,
vals_lr st args args1 args2
-> length args = length args2.
Theorem args_lr_vals_lr : forall st args
(args1 : ctysDenote args) (args2 : list adom) Hlen,
vals_lr st args args1 args2
-> args_lr st args args1
(makeActuals (allocTys args) args2 Hlen).
Hint Resolve args_lr_vals_lr.
Lemma nthFuncs_contra : forall G ts (defs : cfuncs G ts) pos sG,
nthFuncs defs pos = Some sG
-> length (projS1 sG) >= length G.
Theorem allocCode_body_var' : forall G fns (defs : cfuncs G fns)
(ctx : smallCtys) args
(s : Subst ctyDenote G)
(v : Var fns (CCode (proj1_sig ctx) args))
pos (f : cfunc (revAppN fns pos G) (CProd (proj1_sig ctx) :: args)),
nthFuncs defs (length fns - S (allocCode v)) =
Some
(existS (fun G : list cty => sigS (cfunc G))
_ (existS _ (CProd (proj1_sig ctx) :: args) f))
-> VarDenote v (ctysSubst (cfuncsDenote defs s))
= cfuncDenote f
(revAppN_Subst
(ctysSubst (cfuncsDenote defs s)) pos
s).
Theorem allocCode_body_var : forall G fns (defs : cfuncs G fns)
(ctx : smallCtys) args
(G' : list cty)
(s : Subst ctyDenote G)
(s1 : Subst ctyDenote G')
(v : Var (G' ++ fns) (CCode (proj1_sig ctx) args))
pos (f : cfunc (revAppN fns pos G) (CProd (proj1_sig ctx) :: args)),
isSmalls G'
-> nthFuncs defs (length fns - S (allocCode v)) =
Some
(existS (fun G : list cty => sigS (cfunc G))
(revAppN fns pos G)
(existS (cfunc (revAppN fns pos G))
(CProd (proj1_sig ctx) :: args) f))
-> VarDenote v
(appSubst s1
(ctysSubst (cfuncsDenote defs s)))
= cfuncDenote f
(revAppN_Subst
(ctysSubst (cfuncsDenote defs s)) pos
s).
Lemma Var_app_split : forall ts ts' t
(v : Var (ts ++ ts') t),
allocCode v < length ts'
\/ exists v' : Var ts t,
allocCode v = length ts' + allocCode v'.
Lemma Var_revAppN_split : forall pos ts t' t
(v : Var (revAppN ts pos (t' :: nil)) t),
(allocCode v = 0 /\ t' = t)
\/ exists v' : Var (revAppN ts pos nil) t,
allocCode v = S (allocCode v').
Lemma allocCode_nth_revAppN' : forall G fns (defs : cfuncs G fns) pos
ctx args (v : Var (revAppN fns pos nil) (CCode ctx args)),
exists pos', exists f,
pos' < pos
/\ nthFuncs defs (allocCode v)
= Some (existS (fun G => sigS (cfunc G)) (revAppN fns pos' G)
(existS _ (CProd ctx :: args) f)).
Lemma allocCode_nth_revAppN : forall G fns (defs : cfuncs G fns) pos
ctx args G' (v : Var (G' ++ revAppN fns pos nil) (CCode ctx args)),
isSmalls G'
-> exists pos', exists f,
pos' < pos
/\ nthFuncs defs (allocCode v)
= Some (existS (fun G => sigS (cfunc G)) (revAppN fns pos' G)
(existS _ (CProd ctx :: args) f)).
Lemma allocCode_zero' : forall fns t
(v : Var (fns ++ t :: nil) t) x s,
allocCode v = 0
-> VarDenote v (appSubst s (SCons t x (SNil ctyDenote))) = x.
Lemma allocCode_zero : forall fns pos t
(v : Var (revAppN fns pos (t :: nil)) t) x s,
allocCode v = 0
-> VarDenote v (revAppN_Subst s pos (SCons t x (SNil ctyDenote))) = x.
Lemma allocCode_push' : forall G' s t t'
(v' : Var (G' ++ nil) t') (v : Var (G' ++ t :: nil) t') x,
allocCode v = S (allocCode v') ->
VarDenote v' (appSubst s (SNil ctyDenote)) =
VarDenote v (appSubst s (SCons t x (SNil ctyDenote))).
Lemma allocCode_push : forall pos ts t t'
(v : Var (revAppN ts pos (t :: nil)) t')
(v' : Var (revAppN ts pos nil) t') x s,
allocCode v = S (allocCode v')
-> VarDenote v'
(revAppN_Subst s pos (SNil ctyDenote))
= VarDenote v (revAppN_Subst s pos
(SCons t x (SNil ctyDenote))).
Lemma allocProg_funcs_var' : forall G fns (defs : cfuncs G fns)
pos' pos (ctx : smallCtys) args
(v : Var (revAppN fns (pos' + pos) nil) (CCode (proj1_sig ctx) args))
(f : cfunc (revAppN fns pos' G) (CProd (proj1_sig ctx) :: args)) s,
nthFuncs defs (allocCode v) =
Some
(existS (fun G : list cty => sigS (cfunc G))
(revAppN fns pos' G)
(existS (cfunc (revAppN fns pos' G))
(CProd (proj1_sig ctx) :: args) f))
-> cfuncDenote f
(revAppN_Subst
(ctysSubst (cfuncsDenote defs s))
pos' s) =
VarDenote v
(revAppN_Subst
(ctysSubst (cfuncsDenote defs s))
(pos' + pos) (SNil _)).
Lemma allocProg_funcs_var : forall G fns (defs : cfuncs G fns)
pos' pos (ctx : smallCtys) args
(v : Var (revAppN fns pos nil) (CCode (proj1_sig ctx) args))
(f : cfunc (revAppN fns pos' G) (CProd (proj1_sig ctx) :: args)) s,
pos' < pos
-> nthFuncs defs (allocCode v) =
Some
(existS (fun G : list cty => sigS (cfunc G))
(revAppN fns pos' G)
(existS (cfunc (revAppN fns pos' G))
(CProd (proj1_sig ctx) :: args) f))
-> cfuncDenote f
(revAppN_Subst
(ctysSubst (cfuncsDenote defs s))
pos' s) =
VarDenote v
(revAppN_Subst
(ctysSubst (cfuncsDenote defs s))
pos (SNil _)).
Lemma allocProg_funcs_soundness :
forall (posBound pos : nat), pos <= posBound
-> forall (st : mem adom) (ctx : smallCtys)
(args : list cty) G' (s1 : Subst ctyDenote G')
(v : Var (G' ++ revAppN (cFns pr) pos nil) (CCode (proj1_sig ctx) args))
(env1 : ctyDenote (CProd (proj1_sig ctx))) (args1 : ctysDenote args)
(env2 : atyDenote (allocTy (CProd (proj1_sig ctx))))
(args2 : list adom),
isSmalls G'
-> val_lr st (CProd (proj1_sig ctx)) env1 env2
-> vals_lr st args args1 args2
-> runTrace (amakeTrace (allocProg pr) st (S (allocCode v))
(ARef :: allocTys args) ((Traced, env2) :: args2))
(VarDenote v
(appSubst s1
(revAppN_Subst
(ctysSubst
(cfuncsDenote (cDefs pr) (SNil ctyDenote))) pos
(SNil ctyDenote))) (env1, args1)).
Theorem allocProg_body_sound :
allocCode_soundness
(fun (G : list cty) (H : cty) (x : Var G H) =>
length (cFns pr) - S (allocCode x))
(ctysSubst (cfuncsDenote (cDefs pr) (SNil ctyDenote))).
Hypothesis Gpr_smalls : isSmalls Gpr.
Theorem allocProg_sound : prog_lr pr (allocProg pr).
End Traces.