From dcdd233f666fbeab71bb25a6f48bcf3b7d36cbcd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Aug 2018 19:16:34 -0400 Subject: Fix a wrong bound computation (on negatives), fix a proof --- src/Experiments/NewPipeline/AbstractInterpretation.v | 6 +++++- src/Experiments/NewPipeline/Toplevel1.v | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v index 3391c741b..bec6434a1 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretation.v +++ b/src/Experiments/NewPipeline/AbstractInterpretation.v @@ -429,7 +429,11 @@ Module Compilers. => fun v m => match to_literal m, to_literal v with | Some m, Some v => of_literal (ident.interp idc v m) - | Some m, None => Some r[0 ~> m] + | Some m, None => Some (if (0 m-1] + else if (m =? 0)%Z + then r[0 ~> 0] + else r[m+1 ~> 0]) | _, _ => None end | ident.bool_rect _ diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 626fb04f1..727426082 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -1782,6 +1782,7 @@ Module Import UnsaturatedSolinas. { rewrite !map_app in *; cbn [map] in *. erewrite !eval_snoc by (distr_length; eauto). cbn [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by] in *. + cbv [is_bounded_by_bool] in *. specialize_by (intros; auto with omega). specialize (Hwt n); specialize_by omega. repeat first [ progress Bool.split_andb -- cgit v1.2.3