From ef3ce824f87fd11eed78a13a884579499a8ffc53 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 2 Apr 2019 17:51:17 -0400 Subject: Add Z.combine_at_bitwidth --- src/AbstractInterpretation.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/AbstractInterpretation.v') diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v index e74582ae6..0489f4dc8 100644 --- a/src/AbstractInterpretation.v +++ b/src/AbstractInterpretation.v @@ -685,6 +685,12 @@ Module Compilers. (ZRange.four_corners Z.add x y) (ZRange.eight_corners (fun x y m => Z.max 0 (x + y - m)) x y m))) + | ident.Z_combine_at_bitwidth as idc + => fun bitwidth lo hi + => bitwidth <- to_literal bitwidth; + lo <- lo; + hi <- hi; + Some (ZRange.four_corners (ident.interp idc bitwidth) lo hi) | ident.Z_cast range => fun r : option zrange => interp_Z_cast range r -- cgit v1.2.3