diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-05 15:19:03 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-05 15:19:03 -0500 |
commit | f0bfe4784aea55d5e6614c843a25da44329d5807 (patch) | |
tree | 6e69d5eff5815713f4f5c60a94e9dbe45686dabd /src | |
parent | 994f1f78a9fc77767125580fec674d1709071667 (diff) |
Allow reifying Z.cast2
Diffstat (limited to 'src')
-rw-r--r-- | src/Language.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Language.v b/src/Language.v index a686a846b..016ad8b04 100644 --- a/src/Language.v +++ b/src/Language.v @@ -998,6 +998,9 @@ Module Compilers. else if is_more_pos_than_neg r x then cast_outside_of_range' r x else -cast_outside_of_range' (-r) (-x). + Definition cast2 (r : zrange * zrange) (x : BinInt.Z * BinInt.Z) + := (cast (Datatypes.fst r) (Datatypes.fst x), + cast (Datatypes.snd r) (Datatypes.snd x)). Local Notation wordmax log2wordmax := (2 ^ log2wordmax). Local Notation half_bits log2wordmax := (log2wordmax / 2). @@ -1367,6 +1370,7 @@ Module Compilers. | Z.rshi => then_tac ident.Z_rshi | Z.cc_m => then_tac ident.Z_cc_m | ident.cast _ ?r => then_tac (ident.Z_cast r) + | ident.cast2 _ ?r => then_tac (ident.Z_cast2 r) | @Some ?A => let rA := base.reify A in then_tac (@ident.Some rA) |