From 2a3da2e5ff16a89cc19c1c2dbd809c0be7c26484 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Mar 2017 14:15:14 -0400 Subject: Use Bounds in BoundsInterpretations --- src/Reflection/Z/BoundsInterpretations.v | 35 +++----------------------------- 1 file changed, 3 insertions(+), 32 deletions(-) diff --git a/src/Reflection/Z/BoundsInterpretations.v b/src/Reflection/Z/BoundsInterpretations.v index 7327cb180..928402473 100644 --- a/src/Reflection/Z/BoundsInterpretations.v +++ b/src/Reflection/Z/BoundsInterpretations.v @@ -5,6 +5,7 @@ Require Import Crypto.Reflection.Relations. Require Import Crypto.Util.Option. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Bounds. Require Import Crypto.Util.Tactics.DestructHead. Export Reflection.Syntax.Notations. @@ -12,10 +13,6 @@ Local Notation eta x := (fst x, snd x). Local Notation eta3 x := (eta (fst x), snd x). Local Notation eta4 x := (eta3 (fst x), snd x). -Delimit Scope bounds_scope with bounds. -Record bounds := { lower : Z ; upper : Z }. -Bind Scope bounds_scope with bounds. - Module Import Bounds. Definition t := option bounds. (* TODO?: Separate out the bounds computation from the overflow computation? e.g., have [safety := in_bounds | overflow] and [t := bounds * safety]? *) Bind Scope bounds_scope with t. @@ -105,9 +102,7 @@ Module Import Bounds. End with_bitwidth. Module Export Notations. - Delimit Scope bounds_scope with bounds. - Notation "b[ l ~> u ]" := {| lower := l ; upper := u |} - (format "b[ l ~> u ]") : bounds_scope. + Export Util.Bounds.Notations. Infix "+" := (add _) : bounds_scope. Infix "-" := (sub _) : bounds_scope. Infix "*" := (mul _) : bounds_scope. @@ -141,18 +136,6 @@ Module Import Bounds. | Cast _ T => fun x => SmartRebuildBounds (bit_width_of_base_type T) x end%bounds. - Ltac inversion_bounds := - let lower := (eval cbv [lower] in (fun x => lower x)) in - let upper := (eval cbv [upper] in (fun y => upper y)) in - repeat match goal with - | [ H : _ = _ :> bounds |- _ ] - => pose proof (f_equal lower H); pose proof (f_equal upper H); clear H; - cbv beta iota in * - | [ H : _ = _ :> t |- _ ] - => unfold t in H; inversion_option - end. - - Definition ZToBounds (z : Z) : bounds := {| lower := z ; upper := z |}. Definition of_Z (z : Z) : t := Some (ZToBounds z). Definition of_interp t (z : Syntax.interp_base_type t) : interp_base_type t @@ -196,11 +179,7 @@ Module Import Bounds. := fun val bound => match bound with | Some bounds' - => ((0 <=? lower bounds') && (lower bounds' <=? interpToZ val) && (interpToZ val <=? upper bounds')) - && (match bit_width_of_base_type T with - | Some sz => upper bounds' true - end) + => Util.Bounds.is_bounded_byb (bit_width_of_base_type T) bounds' val | None => true end%bool%Z. Definition is_bounded_by' {T} : Syntax.interp_base_type T -> interp_base_type T -> Prop @@ -211,14 +190,6 @@ Module Import Bounds. Definition is_bounded_by_bool {T} : interp_flat_type Syntax.interp_base_type T -> interp_flat_type interp_base_type T -> bool := interp_flat_type_relb_pointwise (@is_bounded_byb). - Global Instance dec_eq_bounds : DecidableRel (@eq bounds) | 10. - Proof. - intros [lx ux] [ly uy]. - destruct (dec (lx = ly)), (dec (ux = uy)); - [ left; apply f_equal2; assumption - | abstract (right; intro H; inversion_bounds; tauto).. ]. - Defined. - Local Arguments interp_base_type !_ / . Global Instance dec_eq_interp_flat_type {T} : DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10. Proof. -- cgit v1.2.3