From 7df5f3cd39e43d0197e58ba528831c6f5bda40b5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 22 Jan 2024 16:15:08 -0500 Subject: [PATCH] Fix DCE/Subst01 to work under lambdas The naive encoding of PHOAS passes that need to produce both [expr]-like output and data-like output simultaneously involves exponential blowup. This commit adds caching of results (and/or intermediates) of a data-producing PHOAS pass in a tree structure that mimics the PHOAS expression so that a subsequent pass can consume this tree and a PHOAS expression to produce a new expression. More concretely, suppose we are trying to write a pass that is `expr var1 * expr var2 -> A * expr var3`. We can define an `expr`-like-tree-structure that (a) doesn't use higher-order things for `Abs` nodes, and (b) stores `A` at every node. Then we can write a pass that is `expr var1 * expr var2 -> A * tree-of-A` and then `expr var1 * expr var2 * tree-of-A -> expr var3` such that we incur only linear overhead. See also #1761 and https://github.com/mit-plv/fiat-crypto/issues/1604#issuecomment-1553341559. Fixes #1604 --- src/BoundsPipeline.v | 10 +- src/Language/TreeCaching.v | 70 +++++++++++++ src/MiscCompilerPasses.v | 147 +++++++++++++++++----------- src/MiscCompilerPassesProofs.v | 95 +++++++++++------- src/MiscCompilerPassesProofsExtra.v | 8 +- 5 files changed, 226 insertions(+), 104 deletions(-) create mode 100644 src/Language/TreeCaching.v diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index 5666bb1945..de40f32702 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -660,12 +660,6 @@ Module Pipeline. (E : Expr t) : DebugM (Expr t) := (E <- DoRewrite E; - (* Note that DCE evaluates the expr with two different [var] - arguments, and so results in a pipeline that is 2x slower - unless we pass through a uniformly concrete [var] type - first *) - dlet_nd e := ToFlat E in - let E := FromFlat e in E <- if with_subst01 return DebugM (Expr t) then wrap_debug_rewrite ("subst01 for " ++ descr) (Subst01.Subst01 ident.is_comment) E else if with_dead_code_elimination return DebugM (Expr t) @@ -675,8 +669,6 @@ Module Pipeline. then wrap_debug_rewrite ("LetBindReturn for " ++ descr) (UnderLets.LetBindReturn (@ident.is_var_like)) E else Debug.ret E; E <- DoRewrite E; (* after inlining, see if any new rewrite redexes are available *) - dlet_nd e := ToFlat E in - let E := FromFlat e in E <- if with_dead_code_elimination then wrap_debug_rewrite ("DCE after " ++ descr) (DeadCodeElimination.EliminateDead ident.is_comment) E else Debug.ret E; @@ -1150,7 +1142,7 @@ Module Pipeline. first [ progress destruct_head'_and | progress cbv [Classes.base Classes.ident Classes.ident_interp Classes.base_interp Classes.exprInfo] in * | progress intros - | progress rewrite_strat repeat topdown hints interp + | progress rewrite_strat repeat topdown choice (hints interp_extra) (hints interp) | solve [ typeclasses eauto with nocore interp_extra wf_extra ] | solve [ typeclasses eauto ] | break_innermost_match_step diff --git a/src/Language/TreeCaching.v b/src/Language/TreeCaching.v new file mode 100644 index 0000000000..107c4d8f09 --- /dev/null +++ b/src/Language/TreeCaching.v @@ -0,0 +1,70 @@ +(** * Tree Caching for PHOAS Expressions *) +(** The naive encoding of PHOAS passes that need to produce both + [expr]-like output and data-like output simultaneously involves + exponential blowup. + + This file allows caching of results (and/or intermediates) of a + data-producing PHOAS pass in a tree structure that mimics the + PHOAS expression so that a subsequent pass can consume this tree + and a PHOAS expression to produce a new expression. + + More concretely, suppose we are trying to write a pass that is + [expr var1 * expr var2 -> A * expr var3]. We can define an + [expr]-like-tree-structure that (a) doesn't use higher-order + things for [Abs] nodes, and (b) stores [A] at every node. Then we + can write a pass that is [expr var1 * expr var2 -> A * tree-of-A] + and then [expr var1 * expr var2 * tree-of-A -> expr var3] such + that we incur only linear overhead. + + See also + %\href{https://github.com/mit-plv/fiat-crypto/issues/1604#issuecomment-1553341559}{mit-plv/fiat-crypto\#1604 with option (2)}% + #mit-plv/fiat-crypto##1604 with option (2)# + and + %\href{https://github.com/mit-plv/fiat-crypto/issues/1761}{mit-plv/fiat-crypto\#1761}% + #mit-plv/fiat-crypto##1761#. *) + +Require Import Rewriter.Language.Language. + +Module Compilers. + Export Language.Compilers. + Local Set Boolean Equality Schemes. + Local Set Decidable Equality Schemes. + + Module tree_nd. + Section with_result. + Context {base_type : Type}. + Local Notation type := (type base_type). + Context {ident : type -> Type} + {result : Type}. + Local Notation expr := (@expr.expr base_type ident). + + Inductive tree : Type := + | Ident (r : result) : tree + | Var (r : result) : tree + | Abs (r : result) (f : option tree) : tree + | App (r : result) (f : option tree) (x : option tree) : tree + | LetIn (r : result) (x : option tree) (f : option tree) : tree + . + End with_result. + Global Arguments tree result : clear implicits, assert. + End tree_nd. + + Module tree. + Section with_result. + Context {base_type : Type}. + Local Notation type := (type base_type). + Context {ident : type -> Type} + {result : type -> Type}. + Local Notation expr := (@expr.expr base_type ident). + + Inductive tree : type -> Type := + | Ident {t} (r : result t) : tree t + | Var {t} (r : result t) : tree t + | Abs {s d} (r : result (s -> d)) (f : option (tree d)) : tree (s -> d) + | App {s d} (r : result d) (f : option (tree (s -> d))) (x : option (tree s)) : tree d + | LetIn {A B} (r : result B) (x : option (tree A)) (f : option (tree B)) : tree B + . + End with_result. + Global Arguments tree {base_type} {result} t, {base_type} result t : assert. + End tree. +End Compilers. diff --git a/src/MiscCompilerPasses.v b/src/MiscCompilerPasses.v index a534f59744..b4e7c64e60 100644 --- a/src/MiscCompilerPasses.v +++ b/src/MiscCompilerPasses.v @@ -3,11 +3,14 @@ Require Import Coq.MSets.MSetPositive. Require Import Coq.FSets.FMapPositive. Require Import Crypto.Util.ListUtil Coq.Lists.List. Require Import Rewriter.Language.Language. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. +Require Import Crypto.Language.TreeCaching. Import ListNotations. Local Open Scope Z_scope. Module Compilers. Export Language.Compilers. + Export Language.TreeCaching.Compilers. Import invert_expr. Module Subst01. @@ -33,6 +36,8 @@ Module Compilers. (** some identifiers, like [comment], might always be live *) (is_ident_always_live : forall t, ident t -> bool). Local Notation expr := (@expr.expr base_type ident). + (* [option t] is "is the let-in here live?", meaningless elsewhere; the thunk is for debugging *) + Local Notation tree := (@tree_nd.tree (option t * (unit -> positive * list (positive * t)))). (** N.B. This does not work well when let-binders are not at top-level *) Fixpoint contains_always_live_ident {var} (dummy : forall t, var t) {t} (e : @expr var t) : bool @@ -46,28 +51,39 @@ Module Compilers. | expr.LetIn tx tC ex eC => contains_always_live_ident dummy ex || contains_always_live_ident dummy (eC (dummy _)) end%bool. + Definition meaningless : option t * (unit -> positive * list (positive * t)) := (None, (fun 'tt => (1%positive, []%list))). + Global Opaque meaningless. Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive) (live : PositiveMap.t _) - : positive * PositiveMap.t _ + : positive * PositiveMap.t _ * option tree := match e with - | expr.Var t v => (cur_idx, PositiveMap_incr v live) - | expr.Ident t idc => (cur_idx, live) + | expr.Var t v + => let '(idx, live) := (cur_idx, PositiveMap_incr v live) in + (idx, live, Some (tree_nd.Var meaningless)) + | expr.Ident t idc + => let '(idx, live) := (cur_idx, live) in + (idx, live, Some (tree_nd.Ident meaningless)) | expr.App s d 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) + => let '(idx, live, f_tree) := @compute_live_counts' _ f cur_idx live in + let '(idx, live, x_tree) := @compute_live_counts' _ x idx live in + (idx, live, Some (tree_nd.App meaningless f_tree x_tree)) | expr.Abs s d f - => let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in - (cur_idx, live) + => let '(idx, live, f_tree) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in + (idx, live, Some (tree_nd.Abs meaningless f_tree)) | expr.LetIn tx tC ex eC - => let '(idx, live) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in + => let '(idx, live, C_tree) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in let live := if contains_always_live_ident (fun _ => cur_idx (* dummy *)) ex then PositiveMap_incr_always_live cur_idx live else live in - if PositiveMap.mem cur_idx live - then @compute_live_counts' tx ex idx live - else (idx, live) + let debug_info := fun 'tt => (Pos.succ cur_idx, PositiveMap.elements live) in + match PositiveMap.find cur_idx live with + | Some x_count + => let '(x_idx, x_live, x_tree) := @compute_live_counts' tx ex idx live in + (x_idx, x_live, Some (tree_nd.LetIn (Some x_count, debug_info) x_tree C_tree)) + | None + => (idx, live, Some (tree_nd.LetIn (None, debug_info) None C_tree)) + end end%bool. - Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)). + Definition compute_live_counts {t} e : option tree := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)). Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _). Section with_var. @@ -79,36 +95,61 @@ Module Compilers. in extraction *) Context (doing_subst_debug : forall T1 T2, T1 -> (unit -> 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 + (should_subst : t -> bool). + (** When [live] is [None], we don't inline anything, just + dropping [var]. This is required for preventing blowup + in inlining lets in unused [LetIn]-bound expressions. + *) + Fixpoint subst0n (live : option tree) {t} (e : @expr (@expr var) t) + : @expr var t := match e with - | expr.Var t v => (cur_idx, v) - | expr.Ident t idc => (cur_idx, expr.Ident idc) + | expr.Var t v => v + | expr.Ident t idc => 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') + => let '(f_live, x_live) + := match live with + | Some (tree_nd.App _ f_live x_live) => (f_live, x_live) + | _ => (None, None) + end%core in + let f' := @subst0n f_live _ f in + let x' := @subst0n x_live _ x in + 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)))) + => let f_tree + := match live with + | Some (tree_nd.Abs _ f_tree) => f_tree + | _ => None + end in + expr.Abs (fun v => @subst0n f_tree _ (f (expr.Var v))) | 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_debug _ _ ex' (fun 'tt => (Pos.succ cur_idx, PositiveMap.elements live)))) - else (Pos.succ cur_idx, expr.LetIn ex' (fun v => eC' (expr.Var v))) + => match live with + | Some (tree_nd.LetIn (x_count, debug_info) x_tree C_tree) + => let ex' := @subst0n x_tree tx ex in + let eC' := fun v => @subst0n C_tree tC (eC v) in + if match x_count with + | Some n => should_subst n + | None => true + end + then eC' (doing_subst_debug _ _ ex' debug_info) + else expr.LetIn ex' (fun v => eC' (expr.Var v)) + | _ + => let ex' := @subst0n None tx ex in + let eC' := fun v => @subst0n None tC (eC v) in + expr.LetIn ex' (fun v => eC' (expr.Var v)) + end end. - - Definition subst0n {t} e : expr t - := snd (@subst0n' t e 1). End with_var. - Definition Subst0n (doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1) (should_subst : t -> bool) {t} (e : expr.Expr t) : expr.Expr t - := fun var => subst0n doing_subst_debug should_subst (ComputeLiveCounts e) (e _). + Section with_transport. + Context {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)}. + (** We pass through [Flat] to ensure that the passed in + [Expr] only gets invoked at a single [var] type *) + Definition Subst0n (doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1) (should_subst : t -> bool) {t} (E : expr.Expr t) : expr.Expr t + := dlet_nd e := GeneralizeVar.ToFlat E in + let E := GeneralizeVar.FromFlat e in + fun var => subst0n doing_subst_debug should_subst (ComputeLiveCounts E) (E _). + End with_transport. End with_ident. End with_counter. @@ -122,8 +163,13 @@ Module Compilers. | more => false end. - Definition Subst01 {base_type ident} (is_ident_always_live : forall t, ident t -> bool) {t} (e : expr.Expr t) : expr.Expr t - := @Subst0n _ one incr (fun _ => more) base_type ident is_ident_always_live (fun _ _ x _ => x) should_subst t e. + Definition Subst01 + {base_type ident} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT _ _} + (is_ident_always_live : forall t, ident t -> bool) + {t} (e : expr.Expr t) : expr.Expr t + := @Subst0n _ one incr (fun _ => more) base_type ident is_ident_always_live try_make_transport_base_type_cps exprDefault (fun _ _ x _ => x) should_subst t e. End for_01. End Subst01. @@ -131,25 +177,16 @@ Module Compilers. Section with_ident. Context {base_type : Type}. Local Notation type := (type.type base_type). - Context {ident : type -> Type} - (is_ident_always_live : forall t, ident t -> bool). - Local Notation expr := (@expr.expr base_type ident). - Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v. Global Opaque OUGHT_TO_BE_UNUSED. - - Definition ComputeLive {t} (e : expr.Expr t) : PositiveMap.t unit - := @Subst01.ComputeLiveCounts unit tt (fun _ => tt) (fun _ => tt) base_type ident is_ident_always_live _ e. - Definition is_live (map : PositiveMap.t unit) (idx : positive) : bool - := match PositiveMap.find idx map with - | Some tt => true - | None => false - end. - Definition is_dead (map : PositiveMap.t unit) (idx : positive) : bool - := negb (is_live map idx). - - Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t - := @Subst01.Subst0n unit tt (fun _ => tt) (fun _ => tt) base_type ident is_ident_always_live (fun T1 T2 => OUGHT_TO_BE_UNUSED) (fun _ => false) t e. + Definition EliminateDead + {ident : type -> Type} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT _ _} + (is_ident_always_live : forall t, ident t -> bool) + {t} (e : expr.Expr t) + : expr.Expr t + := @Subst01.Subst0n unit tt (fun _ => tt) (fun _ => tt) base_type ident is_ident_always_live try_make_transport_base_type_cps exprDefault (fun T1 T2 => OUGHT_TO_BE_UNUSED) (fun _ => false) t e. End with_ident. End DeadCodeElimination. End Compilers. diff --git a/src/MiscCompilerPassesProofs.v b/src/MiscCompilerPassesProofs.v index 0fe5c89638..569bb993a8 100644 --- a/src/MiscCompilerPassesProofs.v +++ b/src/MiscCompilerPassesProofs.v @@ -6,7 +6,10 @@ Require Import Coq.FSets.FMapPositive. Require Import Rewriter.Language.Language. Require Import Rewriter.Language.Inversion. Require Import Rewriter.Language.Wf. +Require Import Crypto.Language.TreeCaching. Require Import Crypto.MiscCompilerPasses. +Require Import Crypto.Util.Bool.Reflect. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. @@ -39,45 +42,42 @@ Module Compilers. Section with_ident. Context {base_type : Type}. Local Notation type := (type.type base_type). - Context {ident : type -> Type} - (is_ident_always_live : forall t, ident t -> bool). + Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). + Context {base_type_beq : base_type -> base_type -> bool} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {reflect_base_type_beq : reflect_rel (@eq base_type) base_type_beq} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + Context (is_ident_always_live : forall t, ident t -> bool). Section with_var. Context {doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1} {should_subst : T -> bool} (Hdoing_subst_debug : forall T1 T2 x y, doing_subst_debug T1 T2 x y = x) - {var1 var2 : type -> Type} - (live : PositiveMap.t T). + {var1 var2 : type -> Type}. + Local Notation tree := (@tree_nd.tree (option T * (unit -> positive * list (positive * 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_debug var1 should_subst live). - Local Notation subst0n'2 := (@subst0n' T base_type ident doing_subst_debug var2 should_subst live). - Local Notation subst0n1 := (@subst0n T base_type ident doing_subst_debug var1 should_subst live). - Local Notation subst0n2 := (@subst0n T base_type ident doing_subst_debug var2 should_subst live). + Local Notation subst0n1 := (@subst0n T base_type ident doing_subst_debug var1 should_subst). + Local Notation subst0n2 := (@subst0n T base_type ident doing_subst_debug var2 should_subst). - Lemma wf_subst0n' G1 G2 t e1 e2 p + Lemma wf_subst0n_gen live G1 G2 t e1 e2 (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). + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (subst0n1 live e1) (subst0n2 live e2). Proof using Hdoing_subst_debug. - intro Hwf; revert dependent G2; revert p; induction Hwf; - cbn [subst0n']; + intro Hwf; revert dependent G2; revert live; induction Hwf; + cbn [subst0n]; repeat first [ progress wf_safe_t | simplifier_t_step - | progress split_and | rewrite Hdoing_subst_debug - | 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_debug. clear -Hdoing_subst_debug; intro Hwf; apply wf_subst0n' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. + Lemma wf_subst0n live t e1 e2 + : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst0n1 live e1) (subst0n2 live e2). + Proof using Hdoing_subst_debug. intro Hwf; eapply wf_subst0n_gen, Hwf; wf_safe_t. Qed. End with_var. Lemma Wf_Subst0n @@ -86,7 +86,10 @@ Module Compilers. (Hdoing_subst_debug : forall T1 T2 x y, doing_subst_debug T1 T2 x y = x) {t} (e : @expr.Expr base_type ident t) : expr.Wf e -> expr.Wf (Subst0n one incr incr_always_live is_ident_always_live doing_subst_debug should_subst e). - Proof using Type. intros Hwf var1 var2; eapply wf_subst0n, Hwf; assumption. Qed. + Proof using try_make_transport_base_type_cps_correct. + intros Hwf var1 var2; cbv [Subst0n Let_In]. + apply wf_subst0n, GeneralizeVar.Wf_FromFlat_ToFlat, Hwf; assumption. + Qed. Section interp. Context {base_interp : base_type -> Type} @@ -98,13 +101,12 @@ Module Compilers. {should_subst : T -> bool} (Hdoing_subst_debug : forall T1 T2 x y, doing_subst_debug T1 T2 x y = x). - Lemma interp_subst0n'_gen (live : PositiveMap.t T) G t (e1 e2 : expr t) + Lemma interp_subst0n_gen live 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_debug should_subst live e1 p)) == expr.interp interp_ident e2. + : expr.interp interp_ident (subst0n doing_subst_debug should_subst live e1) == expr.interp interp_ident e2. Proof using Hdoing_subst_debug interp_ident_Proper. - revert p; induction Hwf; cbn [subst0n']; cbv [Proper respectful] in *; + revert live; induction Hwf; cbn [subst0n]; cbv [Proper respectful] in *; repeat first [ progress interp_safe_t | simplifier_t_step | rewrite Hdoing_subst_debug @@ -115,11 +117,15 @@ Module Compilers. Lemma interp_subst0n live t (e1 e2 : expr t) (Hwf : expr.wf nil e1 e2) : expr.interp interp_ident (subst0n doing_subst_debug should_subst live e1) == expr.interp interp_ident e2. - Proof using Hdoing_subst_debug interp_ident_Proper. clear -Hwf Hdoing_subst_debug interp_ident_Proper. apply interp_subst0n'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + Proof using Hdoing_subst_debug interp_ident_Proper. clear -Hwf Hdoing_subst_debug 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 incr_always_live is_ident_always_live doing_subst_debug should_subst e) == expr.Interp interp_ident e. - Proof using Hdoing_subst_debug interp_ident_Proper. apply interp_subst0n, Hwf. Qed. + Proof using Hdoing_subst_debug interp_ident_Proper try_make_transport_base_type_cps_correct. + cbv [Subst0n Let_In expr.Interp]. + etransitivity; [ apply interp_subst0n, GeneralizeVar.Wf_FromFlat_ToFlat, Hwf | ]. + apply GeneralizeVar.Interp_gen1_FromFlat_ToFlat; assumption. + Qed. End with_doing_subst_debug. End interp. End with_ident. @@ -128,13 +134,18 @@ Module Compilers. Section with_ident. Context {base_type : Type}. Local Notation type := (type.type base_type). - Context {ident : type -> Type} - (is_ident_always_live : forall t, ident t -> bool). + Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). + Context {base_type_beq : base_type -> base_type -> bool} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {reflect_base_type_beq : reflect_rel (@eq base_type) base_type_beq} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + Context (is_ident_always_live : forall t, ident t -> bool). Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t) : expr.Wf e -> expr.Wf (Subst01 is_ident_always_live e). - Proof using Type. eapply Wf_Subst0n; reflexivity. Qed. + Proof using try_make_transport_base_type_cps_correct. eapply Wf_Subst0n; try assumption; reflexivity. Qed. Section interp. Context {base_interp : base_type -> Type} @@ -142,9 +153,11 @@ Module Compilers. {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) : expr.Interp interp_ident (Subst01 is_ident_always_live e) == expr.Interp interp_ident e. - Proof using interp_ident_Proper. apply Interp_Subst0n, Hwf; auto. Qed. + Proof using interp_ident_Proper try_make_transport_base_type_cps_correct. eapply Interp_Subst0n, Hwf; auto. Qed. End interp. End with_ident. + + Ltac autorewrite_interp_side_condition_solver := assumption. End Subst01. #[global] @@ -152,7 +165,7 @@ Module Compilers. #[global] Hint Opaque Subst01.Subst01 : wf interp rewrite. #[global] - Hint Rewrite @Subst01.Interp_Subst01 : interp. + Hint Rewrite @Subst01.Interp_Subst01 using Subst01.autorewrite_interp_side_condition_solver : interp. Module DeadCodeElimination. Import MiscCompilerPasses.Compilers.DeadCodeElimination. @@ -169,13 +182,18 @@ Module Compilers. Section with_ident. Context {base_type : Type}. Local Notation type := (type.type base_type). - Context {ident : type -> Type} - (is_ident_always_live : forall t, ident t -> bool). + Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). + Context {base_type_beq : base_type -> base_type -> bool} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {reflect_base_type_beq : reflect_rel (@eq base_type) base_type_beq} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + Context (is_ident_always_live : forall t, ident t -> bool). Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t) : expr.Wf e -> expr.Wf (EliminateDead is_ident_always_live e). - Proof using Type. apply Subst01.Wf_Subst0n; intros; apply @OUGHT_TO_BE_UNUSED_id. Qed. + Proof using try_make_transport_base_type_cps_correct. eapply Subst01.Wf_Subst0n; auto using @OUGHT_TO_BE_UNUSED_id. Qed. Section interp. Context {base_interp : base_type -> Type} @@ -184,9 +202,10 @@ Module Compilers. Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) : expr.Interp interp_ident (EliminateDead is_ident_always_live e) == expr.Interp interp_ident e. - Proof using interp_ident_Proper. apply Subst01.Interp_Subst0n, Hwf; auto using @OUGHT_TO_BE_UNUSED_id. Qed. + Proof using interp_ident_Proper try_make_transport_base_type_cps_correct. eapply Subst01.Interp_Subst0n, Hwf; auto using @OUGHT_TO_BE_UNUSED_id. Qed. End interp. End with_ident. + Ltac autorewrite_interp_side_condition_solver := Subst01.autorewrite_interp_side_condition_solver. End DeadCodeElimination. #[global] @@ -194,5 +213,5 @@ Module Compilers. #[global] Hint Opaque DeadCodeElimination.EliminateDead : wf interp rewrite. #[global] - Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp. + Hint Rewrite @DeadCodeElimination.Interp_EliminateDead using DeadCodeElimination.autorewrite_interp_side_condition_solver : interp. End Compilers. diff --git a/src/MiscCompilerPassesProofsExtra.v b/src/MiscCompilerPassesProofsExtra.v index 6dfe3e82a1..4e8030f9c4 100644 --- a/src/MiscCompilerPassesProofsExtra.v +++ b/src/MiscCompilerPassesProofsExtra.v @@ -26,8 +26,10 @@ Module Compilers. Module Subst01. Import MiscCompilerPassesProofs.Compilers.Subst01. + Definition Wf_Subst01 is_ident_always_live {t} e Hwf + := @Wf_Subst01 _ ident _ _ _ _ _ is_ident_always_live t e Hwf. Definition Interp_Subst01 is_ident_always_live {t} e Hwf - := @Interp_Subst01 _ ident is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. + := @Interp_Subst01 _ ident _ _ _ _ _ is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. End Subst01. #[global] @@ -40,8 +42,10 @@ Module Compilers. Module DeadCodeElimination. Import MiscCompilerPassesProofs.Compilers.DeadCodeElimination. + Definition Wf_EliminateDead is_ident_always_live {t} e Hwf + := @Wf_EliminateDead _ ident _ _ _ _ _ is_ident_always_live t e Hwf. Definition Interp_EliminateDead is_ident_always_live {t} e Hwf - := @Interp_EliminateDead _ ident is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. + := @Interp_EliminateDead _ ident _ _ _ _ _ is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. End DeadCodeElimination. #[global]