Remove a needless GeneralizeVar.GeneralizeVar

Maybe this is responsible for the performance issue???
mit-plv · Dec 5, 2023 · 4c0aeba · 4c0aeba
1 parent 717fae6
commit 4c0aeba
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 10 deletions.
diff --git a/src/AbstractInterpretation/AbstractInterpretation.v b/src/AbstractInterpretation/AbstractInterpretation.v
@@ -577,7 +577,7 @@ Module Compilers.
              {t} (e : Expr t)
              (bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
     : Expr t
-    := partial.EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations (GeneralizeVar.GeneralizeVar (e _)) bound.
+    := partial.EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e bound.
   Definition PartialEvaluateWithListInfoFromBounds
              {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
              {t} (e : Expr t)

diff --git a/src/AbstractInterpretation/Proofs.v b/src/AbstractInterpretation/Proofs.v
@@ -1507,7 +1507,6 @@ Module Compilers.
       by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]).
     assert (arg2_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg2)
       by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]).
-    rewrite <- (GeneralizeVar.Interp_gen1_GeneralizeVar E) by auto with wf.
     eapply Interp_EvalWithBound; eauto with wf typeclass_instances.
   Qed.
 
@@ -1530,14 +1529,7 @@ Module Compilers.
   Proof.
     cbv [PartialEvaluateWithBounds].
     intros arg1 Harg11 Harg1.
-    rewrite <- Extract_GeneralizeVar; auto with wf typeclass_instances.
-    { eapply @Interp_EvalWithBound; eauto with wf typeclass_instances. }
-    { cbv [Proper] in *.
-      eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1;
-        [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ];
-        [ | refine (fun t x y H => H) ];
-        cbv beta.
-      intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl. }
+    eapply @Interp_EvalWithBound; eauto with wf typeclass_instances.
   Qed.
 
   Lemma Interp_PartialEvaluateWithListInfoFromBounds