Future-proof CompilersTestCases

src/AbstractInterpretation/ZRangeProofs.v

@@ -64,6 +64,23 @@ Module Compilers.
         : ZRange.type.option.is_bounded_by x v = true
           -> type.related_hetero (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v.
         Proof. induction t; cbn in *; intuition congruence. Qed.
+
+        Lemma is_bounded_by_impl_eqv_refl t
+          (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+          : ZRange.type.option.is_bounded_by x v = true
+            -> v == v.
+        Proof. induction t; cbn; try reflexivity; try congruence. Qed.
+
+        Lemma andb_bool_for_each_lhs_of_arrow_is_bounded_by_impl_and_for_each_lhs_of_arrow_eqv_refl t
+          (x : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (v : type.for_each_lhs_of_arrow (type.interp base.interp) t)
+          : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) x v = true
+            -> type.and_for_each_lhs_of_arrow (@type.eqv) v v.
+        Proof.
+          induction t; cbn; [ reflexivity | ].
+          rewrite Bool.andb_true_iff.
+          intros [H0 H1].
+          split; eauto using is_bounded_by_impl_eqv_refl.
+        Qed.
       End option.
     End type.
 
@@ -244,7 +261,7 @@ Module Compilers.
                 -- f_equal. assumption.
                 -- intros v H. apply IH2. assumption.
           Qed.
-          
+
           Local Ltac handle_lt_le_t_step_fast :=
             first [ match goal with
                     | [ H : (?a <= ?b)%Z, H' : (?b <= ?a)%Z |- _ ]

src/CompilersTestCases.v

@@ -63,34 +63,34 @@ Module testrewrite.
                           ((\ x , expr_let y := ##5 in $$y + ($$y + (#ident.fst @ $$x + #ident.snd @ $$x)))
                              @ (##1, ##7))%expr).
 
-  Redirect "log" Eval cbv in partial.eval_with_bound partial.default_relax_zrange false (@ident.is_comment) false
+  Redirect "log" Eval cbv in partial.EvalWithBound partial.default_relax_zrange false (@ident.is_comment) false
                                       (RewriteRules.RewriteNBE RewriteRules.default_opts (fun var =>
                 (\z , ((\ x , expr_let y := ##5 in $$y + ($$z + (#ident.fst @ $$x + #ident.snd @ $$x)))
-                         @ (##1, ##7)))%expr) _)
+                         @ (##1, ##7)))%expr))
                 (Datatypes.Some r[0~>100]%zrange, Datatypes.tt).
 End testrewrite.
 Module testpartial.
   Import expr.
   Import ident.
 
-  Redirect "log" Eval compute in partial.eval
-                          (#ident.fst @ (expr_let x := ##10 in ($$x, $$x)))%expr.
+  Redirect "log" Eval compute in partial.Eval
+                          (fun _ => #ident.fst @ (expr_let x := ##10 in ($$x, $$x)))%expr.
 
   Notation "x + y" := (@expr.Ident base.type ident _ _ (ident.Z_add) @ x @ y)%expr : expr_scope.
 
-  Redirect "log" Eval compute in partial.eval
-                          ((\ x , expr_let y := ##5 in #ident.fst @ $$x + (#ident.fst @ $$x + ($$y + $$y)))
+  Redirect "log" Eval compute in partial.Eval
+                          (fun _ => (\ x , expr_let y := ##5 in #ident.fst @ $$x + (#ident.fst @ $$x + ($$y + $$y)))
                              @ (##1, ##1))%expr.
 
-  Redirect "log" Eval compute in partial.eval
-                          ((\ x , expr_let y := ##5 in $$y + ($$y + (#ident.fst @ $$x + #ident.snd @ $$x)))
+  Redirect "log" Eval compute in partial.Eval
+                          (fun _ => (\ x , expr_let y := ##5 in $$y + ($$y + (#ident.fst @ $$x + #ident.snd @ $$x)))
                              @ (##1, ##7))%expr.
 
 
-  Redirect "log" Eval cbv in partial.eval_with_bound
+  Redirect "log" Eval cbv in partial.EvalWithBound
                 partial.default_relax_zrange
                 false (@ident.is_comment) false
-                (\z , ((\ x , expr_let y := ##5 in $$y + ($$z + (#ident.fst @ $$x + #ident.snd @ $$x)))
+                (fun _ => \z , ((\ x , expr_let y := ##5 in $$y + ($$z + (#ident.fst @ $$x + #ident.snd @ $$x)))
                          @ (##1, ##7)))%expr
                 (Datatypes.Some r[0~>100]%zrange, Datatypes.tt).
 End testpartial.