diff options
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/NewPipeline/MiscCompilerPasses.v | 203 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/MiscCompilerPassesProofs.v | 263 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 7 |
3 files changed, 214 insertions, 259 deletions
diff --git a/src/Experiments/NewPipeline/MiscCompilerPasses.v b/src/Experiments/NewPipeline/MiscCompilerPasses.v index 66dd7c09c..d04d4c742 100644 --- a/src/Experiments/NewPipeline/MiscCompilerPasses.v +++ b/src/Experiments/NewPipeline/MiscCompilerPasses.v @@ -11,137 +11,108 @@ Module Compilers. Import invert_expr. Import defaults. - Module DeadCodeElimination. - Section with_ident. - Context {base_type : Type}. - Local Notation type := (type.type base_type). - Context {ident : type -> Type}. - Local Notation expr := (@expr.expr base_type ident). - Fixpoint compute_live' {t} (e : @expr (fun _ => PositiveSet.t) t) (cur_idx : positive) - : positive * PositiveSet.t - := match e with - | expr.Var t v => (cur_idx, v) - | expr.App s d f x - => let '(idx, live1) := @compute_live' _ f cur_idx in - let '(idx, live2) := @compute_live' _ x idx in - (idx, PositiveSet.union live1 live2) - | expr.Abs s d f - => let '(_, live) := @compute_live' _ (f PositiveSet.empty) cur_idx in - (cur_idx, live) - | expr.LetIn tx tC ex eC - => let '(idx, live) := @compute_live' tx ex cur_idx in - let '(_, live) := @compute_live' tC (eC (PositiveSet.add idx live)) (Pos.succ idx) in - (Pos.succ idx, live) - | expr.Ident t idc => (cur_idx, PositiveSet.empty) - end. - Definition compute_live {t} e : PositiveSet.t := snd (@compute_live' t e 1). - Definition ComputeLive {t} (e : expr.Expr t) := compute_live (e _). + Module Subst01. + Section with_counter. + Context {t : Type} + (one : t) + (incr : t -> t). - Section with_var. - Context {var : type -> Type} - (live : PositiveSet.t). - Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v. - Global Opaque OUGHT_TO_BE_UNUSED. - Fixpoint eliminate_dead' {t} (e : @expr (@expr var) t) (cur_idx : positive) - : positive * @expr var t + Local Notation PositiveMap_incr idx m + := (PositiveMap.add idx (match PositiveMap.find idx m with + | Some n => incr n + | None => one + end) m). + + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + (** N.B. This does not work well when let-binders are not at top-level *) + Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive) (live : PositiveMap.t _) + : positive * PositiveMap.t _ := match e with - | expr.Var t v => (cur_idx, v) - | expr.Ident t idc => (cur_idx, expr.Ident idc) + | expr.Var t v => (cur_idx, PositiveMap_incr v live) + | expr.Ident t idc => (cur_idx, live) | expr.App s d f x - => let '(idx, f') := @eliminate_dead' _ f cur_idx in - let '(idx, x') := @eliminate_dead' _ x idx in - (idx, expr.App f' x') + => let '(idx, live) := @compute_live_counts' _ f cur_idx live in + let '(idx, live) := @compute_live_counts' _ x idx live in + (idx, live) | expr.Abs s d f - => (cur_idx, expr.Abs (fun v => snd (@eliminate_dead' _ (f (expr.Var v)) cur_idx))) + => let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in + (cur_idx, live) | expr.LetIn tx tC ex eC - => let '(idx, ex') := @eliminate_dead' tx ex cur_idx in - let eC' := fun v => snd (@eliminate_dead' _ (eC v) (Pos.succ idx)) in - if PositiveSet.mem idx live - then (Pos.succ idx, expr.LetIn ex' (fun v => eC' (expr.Var v))) - else (Pos.succ idx, eC' (OUGHT_TO_BE_UNUSED ex' (Pos.succ idx, PositiveSet.elements live))) + => let '(idx, live) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in + if PositiveMap.mem cur_idx live + then @compute_live_counts' tx ex idx live + else (idx, live) end. + Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)). + Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _). - Definition eliminate_dead {t} e : expr t - := snd (@eliminate_dead' t e 1). - End with_var. + Section with_var. + Context (doing_subst : forall T1 T2, T1 -> T2 -> T1) + {var : type -> Type} + (should_subst : t -> bool) + (live : PositiveMap.t t). + Fixpoint subst0n' {t} (e : @expr (@expr var) t) (cur_idx : positive) + : positive * @expr var t + := match e with + | expr.Var t v => (cur_idx, v) + | expr.Ident t idc => (cur_idx, expr.Ident idc) + | expr.App s d f x + => let '(idx, f') := @subst0n' _ f cur_idx in + let '(idx, x') := @subst0n' _ x idx in + (idx, expr.App f' x') + | expr.Abs s d f + => (cur_idx, expr.Abs (fun v => snd (@subst0n' _ (f (expr.Var v)) (Pos.succ cur_idx)))) + | expr.LetIn tx tC ex eC + => let '(idx, ex') := @subst0n' tx ex cur_idx in + let eC' := fun v => snd (@subst0n' tC (eC v) (Pos.succ cur_idx)) in + if match PositiveMap.find cur_idx live with + | Some n => should_subst n + | None => true + end + then (Pos.succ cur_idx, eC' (doing_subst _ _ ex' (Pos.succ cur_idx, PositiveMap.elements live))) + else (Pos.succ cur_idx, expr.LetIn ex' (fun v => eC' (expr.Var v))) + end. - Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t - := fun var => eliminate_dead (ComputeLive e) (e _). - End with_ident. - End DeadCodeElimination. + Definition subst0n {t} e : expr t + := snd (@subst0n' t e 1). + End with_var. - Module Subst01. - Local Notation PositiveMap_incr idx m - := (PositiveMap.add idx (match PositiveMap.find idx m with - | Some n => S n - | None => S O - end) m). - Local Notation PositiveMap_union m1 m2 - := (PositiveMap.map2 - (fun c1 c2 - => match c1, c2 with - | Some n1, Some n2 => Some (n1 + n2)%nat - | Some n, None - | None, Some n - => Some n - | None, None => None - end) m1 m2). + Definition Subst0n (doing_subst : forall T1 T2, T1 -> T2 -> T1) (should_subst : t -> bool) {t} (e : expr.Expr t) : expr.Expr t + := fun var => subst0n doing_subst should_subst (ComputeLiveCounts e) (e _). + End with_ident. + End with_counter. + + Section for_01. + Inductive one_or_more := one | more. + Local Notation t := one_or_more. + Let incr : t -> t := fun _ => more. + Let should_subst : t -> bool + := fun v => match v with + | one => true + | more => false + end. + + Definition Subst01 {base_type ident} {t} (e : expr.Expr t) : expr.Expr t + := @Subst0n _ one incr base_type ident (fun _ _ x _ => x) should_subst t e. + End for_01. + End Subst01. + + Module DeadCodeElimination. Section with_ident. Context {base_type : Type}. Local Notation type := (type.type base_type). Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). - Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive) - : positive * PositiveMap.t nat - := match e with - | expr.Var t v => (cur_idx, PositiveMap_incr v (PositiveMap.empty _)) - | expr.Ident t idc => (cur_idx, PositiveMap.empty _) - | expr.App s d f x - => let '(idx, live1) := @compute_live_counts' _ f cur_idx in - let '(idx, live2) := @compute_live_counts' _ x idx in - (idx, PositiveMap_union live1 live2) - | expr.Abs s d f - => let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) in - (cur_idx, live) - | expr.LetIn tx tC ex eC - => let '(idx, live1) := @compute_live_counts' tx ex cur_idx in - let '(idx, live2) := @compute_live_counts' tC (eC idx) (Pos.succ idx) in - (idx, PositiveMap_union live1 live2) - end. - Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1). - Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _). - Section with_var. - Context {var : type -> Type} - (live : PositiveMap.t nat). - Fixpoint subst01' {t} (e : @expr (@expr var) t) (cur_idx : positive) - : positive * @expr var t - := match e with - | expr.Var t v => (cur_idx, v) - | expr.Ident t idc => (cur_idx, expr.Ident idc) - | expr.App s d f x - => let '(idx, f') := @subst01' _ f cur_idx in - let '(idx, x') := @subst01' _ x idx in - (idx, expr.App f' x') - | expr.Abs s d f - => (cur_idx, expr.Abs (fun v => snd (@subst01' _ (f (expr.Var v)) (Pos.succ cur_idx)))) - | expr.LetIn tx tC ex eC - => let '(idx, ex') := @subst01' tx ex cur_idx in - let eC' := fun v => snd (@subst01' tC (eC v) (Pos.succ idx)) in - if match PositiveMap.find idx live with - | Some n => (n <=? 1)%nat - | None => true - end - then (Pos.succ idx, eC' ex') - else (Pos.succ idx, expr.LetIn ex' (fun v => eC' (expr.Var v))) - end. - - Definition subst01 {t} e : expr t - := snd (@subst01' t e 1). - End with_var. + Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v. + Global Opaque OUGHT_TO_BE_UNUSED. - Definition Subst01 {t} (e : expr.Expr t) : expr.Expr t - := fun var => subst01 (ComputeLiveCounts e) (e _). + Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t + := @Subst01.Subst0n unit tt (fun _ => tt) base_type ident (@OUGHT_TO_BE_UNUSED) (fun _ => false) t e. End with_ident. - End Subst01. + End DeadCodeElimination. End Compilers. diff --git a/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v index 52101023a..986bfaaa5 100644 --- a/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v +++ b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v @@ -24,22 +24,105 @@ Module Compilers. Import invert_expr. Import defaults. - Module DeadCodeElimination. - Import MiscCompilerPasses.Compilers.DeadCodeElimination. - - (** Rather than proving correctness of the computation of live - variables and requiring something about [live], we instead - rely on the fact that DCE in fact just inlines code it - believes to be dead. *) - Local Transparent OUGHT_TO_BE_UNUSED. - Lemma OUGHT_TO_BE_UNUSED_id {T1 T2} (v : T1) (v' : T2) : OUGHT_TO_BE_UNUSED v v' = v. - Proof. exact eq_refl. Qed. - Local Opaque OUGHT_TO_BE_UNUSED. + Module Subst01. + Import MiscCompilerPasses.Compilers.Subst01. Local Ltac simplifier_t_step := first [ progress cbn [fst snd] in * - | progress eta_expand - | rewrite OUGHT_TO_BE_UNUSED_id ]. + | progress eta_expand ]. + + Section with_counter. + Context {T : Type} + (one : T) + (incr : T -> T). + + Section with_ident. + Context {base_type : Type}. + Local Notation type := (type.type base_type). + Context {ident : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + + Section with_var. + Context {doing_subst : forall T1 T2, T1 -> T2 -> T1} + {should_subst : T -> bool} + (Hdoing_subst : forall T1 T2 x y, doing_subst T1 T2 x y = x) + {var1 var2 : type -> Type} + (live : PositiveMap.t T). + Local Notation expr1 := (@expr.expr base_type ident var1). + Local Notation expr2 := (@expr.expr base_type ident var2). + Local Notation subst0n'1 := (@subst0n' T base_type ident doing_subst var1 should_subst live). + Local Notation subst0n'2 := (@subst0n' T base_type ident doing_subst var2 should_subst live). + Local Notation subst0n1 := (@subst0n T base_type ident doing_subst var1 should_subst live). + Local Notation subst0n2 := (@subst0n T base_type ident doing_subst var2 should_subst live). + + Lemma wf_subst0n' G1 G2 t e1 e2 p + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst0n'1 e1 p)) (snd (subst0n'2 e2 p)) + /\ fst (subst0n'1 e1 p) = fst (subst0n'2 e2 p). + Proof using Hdoing_subst. + intro Hwf; revert dependent G2; revert p; induction Hwf; + cbn [subst0n']; + repeat first [ progress wf_safe_t + | simplifier_t_step + | progress split_and + | rewrite Hdoing_subst + | apply conj + | match goal with + | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto + end + | break_innermost_match_step + | solve [ wf_t ] ]. + Qed. + + Lemma wf_subst0n t e1 e2 + : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst0n1 e1) (subst0n2 e2). + Proof using Hdoing_subst. clear -Hdoing_subst; intro Hwf; apply wf_subst0n' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. + End with_var. + + Lemma Wf_Subst0n + {doing_subst : forall T1 T2, T1 -> T2 -> T1} + {should_subst : T -> bool} + (Hdoing_subst : forall T1 T2 x y, doing_subst T1 T2 x y = x) + {t} (e : @expr.Expr base_type ident t) + : expr.Wf e -> expr.Wf (Subst0n one incr doing_subst should_subst e). + Proof using Type. intros Hwf var1 var2; eapply wf_subst0n, Hwf; assumption. Qed. + + Section interp. + Context {base_interp : base_type -> Type} + {interp_ident : forall t, ident t -> type.interp base_interp t} + {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. + + Section with_doing_subst. + Context {doing_subst : forall T1 T2, T1 -> T2 -> T1} + {should_subst : T -> bool} + (Hdoing_subst : forall T1 T2 x y, doing_subst T1 T2 x y = x). + + Lemma interp_subst0n'_gen (live : PositiveMap.t T) G t (e1 e2 : expr t) + (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) + (Hwf : expr.wf G e1 e2) + p + : expr.interp interp_ident (snd (subst0n' doing_subst should_subst live e1 p)) == expr.interp interp_ident e2. + Proof using Hdoing_subst interp_ident_Proper. + revert p; induction Hwf; cbn [subst0n']; cbv [Proper respectful] in *; + repeat first [ progress interp_safe_t + | simplifier_t_step + | rewrite Hdoing_subst + | break_innermost_match_step + | interp_unsafe_t_step ]. + Qed. + + Lemma interp_subst0n live t (e1 e2 : expr t) + (Hwf : expr.wf nil e1 e2) + : expr.interp interp_ident (subst0n doing_subst should_subst live e1) == expr.interp interp_ident e2. + Proof using Hdoing_subst interp_ident_Proper. clear -Hwf Hdoing_subst interp_ident_Proper. apply interp_subst0n'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + + Lemma Interp_Subst0n {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (Subst0n one incr doing_subst should_subst e) == expr.Interp interp_ident e. + Proof using Hdoing_subst interp_ident_Proper. apply interp_subst0n, Hwf. Qed. + End with_doing_subst. + End interp. + End with_ident. + End with_counter. Section with_ident. Context {base_type : Type}. @@ -47,82 +130,35 @@ Module Compilers. Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). - Section with_var. - Context {var1 var2 : type -> Type} - (live : PositiveSet.t). - Local Notation expr1 := (@expr.expr base_type ident var1). - Local Notation expr2 := (@expr.expr base_type ident var2). - Local Notation eliminate_dead'1 := (@eliminate_dead' base_type ident var1 live). - Local Notation eliminate_dead'2 := (@eliminate_dead' base_type ident var2 live). - Local Notation eliminate_dead1 := (@eliminate_dead base_type ident var1 live). - Local Notation eliminate_dead2 := (@eliminate_dead base_type ident var2 live). - - Lemma wf_eliminate_dead' G1 G2 t e1 e2 p - (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) - : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (eliminate_dead'1 e1 p)) (snd (eliminate_dead'2 e2 p)) - /\ fst (eliminate_dead'1 e1 p) = fst (eliminate_dead'2 e2 p). - Proof. - intro Hwf; revert dependent G2; revert p; induction Hwf; - cbn [eliminate_dead']; - repeat first [ progress wf_safe_t - | simplifier_t_step - | progress split_and - | apply conj - | match goal with - | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto - end - | break_innermost_match_step - | solve [ wf_t ] ]. - Qed. - - Lemma wf_eliminate_dead t e1 e2 - : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (eliminate_dead1 e1) (eliminate_dead2 e2). - Proof. intro Hwf; apply wf_eliminate_dead' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. - End with_var. - - Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t) - : expr.Wf e -> expr.Wf (EliminateDead e). - Proof. intros Hwf var1 var2; eapply wf_eliminate_dead, Hwf. Qed. + Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t) + : expr.Wf e -> expr.Wf (Subst01 e). + Proof using Type. eapply Wf_Subst0n; reflexivity. Qed. Section interp. Context {base_interp : base_type -> Type} {interp_ident : forall t, ident t -> type.interp base_interp t} {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. - - Lemma interp_eliminate_dead'_gen (live : PositiveSet.t) G t (e1 e2 : expr t) - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) - (Hwf : expr.wf G e1 e2) - p - : expr.interp interp_ident (snd (eliminate_dead' live e1 p)) == expr.interp interp_ident e2. - Proof. - revert p; induction Hwf; cbn [eliminate_dead']; cbv [Proper respectful] in *; - repeat first [ progress interp_safe_t - | simplifier_t_step - | break_innermost_match_step - | interp_unsafe_t_step ]. - Qed. - - Lemma interp_eliminate_dead live t (e1 e2 : expr t) - (Hwf : expr.wf nil e1 e2) - : expr.interp interp_ident (eliminate_dead live e1) == expr.interp interp_ident e2. - Proof. apply interp_eliminate_dead'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. - - Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (EliminateDead e) == expr.Interp interp_ident e. - Proof. apply interp_eliminate_dead, Hwf. Qed. + Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (Subst01 e) == expr.Interp interp_ident e. + Proof using interp_ident_Proper. apply Interp_Subst0n, Hwf; auto. Qed. End interp. End with_ident. - End DeadCodeElimination. + End Subst01. - Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf. - Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp. + Hint Resolve Subst01.Wf_Subst01 : wf. + Hint Rewrite @Subst01.Interp_Subst01 : interp. - Module Subst01. - Import MiscCompilerPasses.Compilers.Subst01. + Module DeadCodeElimination. + Import MiscCompilerPasses.Compilers.DeadCodeElimination. - Local Ltac simplifier_t_step := - first [ progress cbn [fst snd] in * - | progress eta_expand ]. + (** Rather than proving correctness of the computation of live + variables and requiring something about [live], we instead + rely on the fact that DCE in fact just inlines code it + believes to be dead. *) + Local Transparent OUGHT_TO_BE_UNUSED. + Lemma OUGHT_TO_BE_UNUSED_id {T1 T2} (v : T1) (v' : T2) : OUGHT_TO_BE_UNUSED v v' = v. + Proof. exact eq_refl. Qed. + Local Opaque OUGHT_TO_BE_UNUSED. Section with_ident. Context {base_type : Type}. @@ -130,73 +166,22 @@ Module Compilers. Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). - Section with_var. - Context {var1 var2 : type -> Type} - (live : PositiveMap.t nat). - Local Notation expr1 := (@expr.expr base_type ident var1). - Local Notation expr2 := (@expr.expr base_type ident var2). - Local Notation subst01'1 := (@subst01' base_type ident var1 live). - Local Notation subst01'2 := (@subst01' base_type ident var2 live). - Local Notation subst011 := (@subst01 base_type ident var1 live). - Local Notation subst012 := (@subst01 base_type ident var2 live). - - Lemma wf_subst01' G1 G2 t e1 e2 p - (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) - : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst01'1 e1 p)) (snd (subst01'2 e2 p)) - /\ fst (subst01'1 e1 p) = fst (subst01'2 e2 p). - Proof. - intro Hwf; revert dependent G2; revert p; induction Hwf; - cbn [subst01']; - repeat first [ progress wf_safe_t - | simplifier_t_step - | progress split_and - | apply conj - | match goal with - | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto - end - | break_innermost_match_step - | solve [ wf_t ] ]. - Qed. - - Lemma wf_subst01 t e1 e2 - : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst011 e1) (subst012 e2). - Proof. intro Hwf; apply wf_subst01' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. - End with_var. - - Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t) - : expr.Wf e -> expr.Wf (Subst01 e). - Proof. intros Hwf var1 var2; eapply wf_subst01, Hwf. Qed. + Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t) + : expr.Wf e -> expr.Wf (EliminateDead e). + Proof using Type. apply Subst01.Wf_Subst0n, @OUGHT_TO_BE_UNUSED_id. Qed. Section interp. Context {base_interp : base_type -> Type} {interp_ident : forall t, ident t -> type.interp base_interp t} {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. - Lemma interp_subst01'_gen (live : PositiveMap.t nat) G t (e1 e2 : expr t) - (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) - (Hwf : expr.wf G e1 e2) - p - : expr.interp interp_ident (snd (subst01' live e1 p)) == expr.interp interp_ident e2. - Proof. - revert p; induction Hwf; cbn [subst01']; cbv [Proper respectful] in *; - repeat first [ progress interp_safe_t - | simplifier_t_step - | break_innermost_match_step - | interp_unsafe_t_step ]. - Qed. - - Lemma interp_subst01 live t (e1 e2 : expr t) - (Hwf : expr.wf nil e1 e2) - : expr.interp interp_ident (subst01 live e1) == expr.interp interp_ident e2. - Proof. apply interp_subst01'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. - - Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) - : expr.Interp interp_ident (Subst01 e) == expr.Interp interp_ident e. - Proof. apply interp_subst01, Hwf. Qed. + Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) + : expr.Interp interp_ident (EliminateDead e) == expr.Interp interp_ident e. + Proof using interp_ident_Proper. apply Subst01.Interp_Subst0n, Hwf; auto using @OUGHT_TO_BE_UNUSED_id. Qed. End interp. End with_ident. - End Subst01. + End DeadCodeElimination. - Hint Resolve Subst01.Wf_Subst01 : wf. - Hint Rewrite @Subst01.Interp_Subst01 : interp. + Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf. + Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp. End Compilers. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index b1bf23019..8cf5687e6 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -688,10 +688,9 @@ Module Pipeline. first *) dlet_nd e := ToFlat E in let E := FromFlat e in - let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in - dlet_nd e := ToFlat E in - let E := FromFlat e in - let E := if with_subst01 then Subst01.Subst01 E else E in + let E := if with_subst01 then Subst01.Subst01 E + else if with_dead_code_elimination then DeadCodeElimination.EliminateDead E + else E in let E := UnderLets.LetBindReturn E in let E := DoRewrite E in (* after inlining, see if any new rewrite redexes are available *) dlet_nd e := ToFlat E in |