Refactor/generalize some pipeline definitions/proofs

When we do rewriting after casts, we will need to do extra passes of DCE
and subst01 to fully reduce things, so we generalize some of the interp
proofs over cast behavior.

For ease of rewriting, we make [ident.interp] an alias (notation) for
[ident.gen_interp], rather than a [Definition].

We also factor out the rewriting wrapper inside the pipeline module into
its own definition.

1 files changed, 52 insertions, 17 deletions

diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 59ce4a33e..ac6cd218d 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -675,6 +675,30 @@ Module Pipeline.
 
   Record to_fancy_args := { invert_low : Z (*log2wordmax*) -> Z -> option Z ; invert_high : Z (*log2wordmax*) -> Z -> option Z }.
 
+  Definition RewriteAndEliminateDeadAndInline {t}
+             (DoRewrite : Expr t -> Expr t)
+             (with_dead_code_elimination : bool)
+             (with_subst01 : bool)
+             (E : Expr t)
+    : Expr t
+    := let E := DoRewrite E in
+       (* 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
+       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 := 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
+       let E := FromFlat e in
+       let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
+       E.
+
   Definition BoundsPipeline
              (with_dead_code_elimination : bool := true)
              (with_subst01 : bool)
@@ -688,22 +712,7 @@ Module Pipeline.
     := (*let E := expr.Uncurry E in*)
       let E := PartialEvaluateWithListInfoFromBounds E arg_bounds in
       let E := PartialEvaluate E in
-      let E := RewriteRules.RewriteArith 0 E in
-      (* 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
-      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 := UnderLets.LetBindReturn E in
-      let E := RewriteRules.RewriteArith 0 E in (* after inlining, see if any new rewrite redexes are available *)
-      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
+      let E := RewriteAndEliminateDeadAndInline (RewriteRules.RewriteArith 0) with_dead_code_elimination with_subst01 E in
       let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *)
       let E := match translate_to_fancy with
                | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E
@@ -788,7 +797,8 @@ Module Pipeline.
                  | solve [ auto with interp wf ]
                  | solve [ typeclasses eauto ]
                  | break_innermost_match_step
-                 | solve [ auto 100 with wf ] ].
+                 | solve [ auto 100 with wf ]
+                 | progress intros ].
 
   Class bounds_goodT {t} bounds
     := bounds_good :
@@ -800,6 +810,30 @@ Module Pipeline.
 
   Hint Extern 1 (type_goodT _) => vm_compute; reflexivity : typeclass_instances.
 
+  Lemma Wf_RewriteAndEliminateDeadAndInline {t} DoRewrite with_dead_code_elimination with_subst01
+        (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E))
+        E
+        (Hwf : Wf E)
+    : Wf (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E).
+  Proof. cbv [RewriteAndEliminateDeadAndInline Let_In]; wf_interp_t. Qed.
+
+  Global Hint Resolve @Wf_RewriteAndEliminateDeadAndInline : wf.
+
+  Lemma Interp_RewriteAndEliminateDeadAndInline {cast_outside_of_range} {t} DoRewrite with_dead_code_elimination with_subst01
+        (Interp_DoRewrite : forall E, Wf E -> expr.Interp (@ident.gen_interp cast_outside_of_range) (DoRewrite E) == expr.Interp (@ident.gen_interp cast_outside_of_range) E)
+        (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E))
+        E
+        (Hwf : Wf E)
+    : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E)
+      == expr.Interp (@ident.gen_interp cast_outside_of_range) E.
+  Proof.
+    cbv [RewriteAndEliminateDeadAndInline Let_In];
+      repeat (wf_interp_t || rewrite !Interp_DoRewrite).
+  Qed.
+
+  Global Hint Rewrite @Interp_RewriteAndEliminateDeadAndInline : interp.
+
+  Local Opaque RewriteAndEliminateDeadAndInline.
   Lemma BoundsPipeline_correct
              (with_dead_code_elimination : bool := true)
              (with_subst01 : bool)
@@ -862,6 +896,7 @@ Module Pipeline.
         all: wf_interp_t. }
       { wf_interp_t. } }
   Qed.
+  Local Transparent RewriteAndEliminateDeadAndInline.
 
   Definition BoundsPipeline_correct_transT
              {t}