diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/mono_rewrites.sail | 4 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index b38e7935..81d42663 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -8,9 +8,9 @@ $include <vector_dec.sail> /* External definitions not in the usual asl prelude */ -val extzv = "extz_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extzv = "extz_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure -val extsv = "exts_vec" : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +val extsv = "exts_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure /* This is generated internally to deal with case splits which reveal the size of a bitvector */ diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 959044a1..6014ab8c 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -41,7 +41,7 @@ val count_leading_zeros = "count_leading_zeros" : forall 'N , 'N >= 1. bits('N) /* function count_leading_zeros x = { foreach (i from ('N - 1) to 0 by 1 in dec) - if [x[i]] == 0b1 then return 'N - i - 1; + if [x[i]] == [bitone] then return 'N - i - 1; return 'N; } */ @@ -217,7 +217,7 @@ function slice_mask(n,i,l) = if l >= n then { sail_shiftleft(sail_ones(n), i) } else { - let one : bits('n) = sail_mask(n, 0b1 : bits(1)) in + let one : bits('n) = sail_mask(n, [bitone] : bits(1)) in sail_shiftleft(sub_bits(sail_shiftleft(one, l), one), i) } |