diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-23 15:31:59 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-23 15:31:59 -0500 |
commit | fbc9433c5a4c48ec3d2367246aa50e28baddd476 (patch) | |
tree | 5a2b46341fd3062a4b0d84e47706a87d7530ce1c /src/Util/ZRange/Operations.v | |
parent | 9d1319323dfc8a788832aaa8e682eabc084bcafa (diff) |
Add some bounds operations to ZRange
Diffstat (limited to 'src/Util/ZRange/Operations.v')
-rw-r--r-- | src/Util/ZRange/Operations.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 71dc31e50..a127568cf 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -3,6 +3,7 @@ Require Import Crypto.Util.ZRange. Require Import Crypto.Util.Notations. Module ZRange. + Local Open Scope Z_scope. Local Open Scope zrange_scope. Local Notation eta v := r[ lower v ~> upper v ]. @@ -53,4 +54,32 @@ Module ZRange. := let (lx, ux) := eta x in union (four_corners (f lx) y z) (four_corners (f ux) y z). + + Definition upper_lor_and_bounds (x y : BinInt.Z) : BinInt.Z + := 2^(1 + Z.log2_up (Z.max x y)). + Definition extreme_lor_land_bounds (x y : zrange) : zrange + := let mx := ZRange.upper (ZRange.abs x) in + let my := ZRange.upper (ZRange.abs y) in + {| lower := -upper_lor_and_bounds mx my ; upper := upper_lor_and_bounds mx my |}. + Definition extremization_bounds (f : zrange -> zrange -> zrange) (x y : zrange) : zrange + := let (lx, ux) := x in + let (ly, uy) := y in + if ((lx <? 0) || (ly <? 0))%Z%bool + then extreme_lor_land_bounds x y + else f x y. + Definition land_bounds : zrange -> zrange -> zrange + := extremization_bounds + (fun x y + => let (lx, ux) := x in + let (ly, uy) := y in + {| lower := Z.min 0 (Z.min lx ly) ; upper := Z.max 0 (Z.min ux uy) |}). + + Definition split_bounds (r : zrange) (split_at : BinInt.Z) : zrange * zrange := + if upper r <? split_at + then if (0 <=? lower r)%Z + then (r, {| lower := 0; upper := 0 |}) + else ( {| lower := 0; upper := split_at - 1 |}, + {| lower := 0; upper := Z.max ( -(lower r / split_at)) (upper r / split_at) |} ) + else ( {| lower := 0; upper := split_at - 1 |}, + {| lower := 0; upper := Z.max ( -(lower r / split_at)) (upper r / split_at) |} ). End ZRange. |