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]