diff options
| author | Brian Campbell | 2018-04-18 14:32:39 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-04-18 14:34:29 +0100 |
| commit | d2e1042f01099e11e04cbfe9529c32db41363e1a (patch) | |
| tree | a10179b026f53cfea4df38c1cebc5622de96239c /aarch64 | |
| parent | 7cab45aa4faac2990eb5e1991c0481b72e3c83ec (diff) | |
Move Lem shl_int, shr_int implementations from aarch64_extras to sail lib
(note that they're already declared in lib/arith.sail)
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/aarch64_extras.lem | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem index 58f1b9c7..c9ea84e2 100644 --- a/aarch64/aarch64_extras.lem +++ b/aarch64/aarch64_extras.lem @@ -60,12 +60,6 @@ let exts_slice v i j = ext_slice true v i j val extz_slice : list bitU -> integer -> integer -> list bitU let extz_slice v i j = ext_slice false v i j*) -val shr_int : ii -> ii -> ii -let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x - -val shl_int : integer -> integer -> integer -let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i - let hexchar_to_bool_list c = if c = #'0' then Just ([false;false;false;false]) else if c = #'1' then Just ([false;false;false;true ]) |
