Skip to content

Commit

Permalink
Future-proof CompilersTestCases (#1762)
Browse files Browse the repository at this point in the history
Also add some utility functions to ZRangeProofs

This is very minor progress towards avoiding replacing the abstract
state of higher order functions with bottom when we can avoid it, in
service of #1609.
  • Loading branch information
JasonGross authored Dec 3, 2023
1 parent 4f20f8d commit 1e57389
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 11 deletions.
19 changes: 18 additions & 1 deletion src/AbstractInterpretation/ZRangeProofs.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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 |- _ ]
Expand Down
20 changes: 10 additions & 10 deletions src/CompilersTestCases.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 1e57389

Please sign in to comment.