diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 14 | ||||
| -rw-r--r-- | src/test/power.sail | 7 |
2 files changed, 12 insertions, 9 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 9a183f7f..2a1095b6 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -31,10 +31,11 @@ let bool_to_bit b = match b with * By convention, MSB is on the left, so increasing = Big-Endian (MSB0), * hence MSB first. * http://en.wikipedia.org/wiki/Bit_numbering *) -(* XXX signedness probably broken here *) -let to_num_inc (V_vector idx true l) = - V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool (reverse l)))))) Unknown);; -let to_num_dec (V_vector idx false l) = +let to_num signed (V_vector idx inc l) = + (* Word library in Lem expects bitseq with LSB first *) + let l = if inc then reverse l else l in + (* Make sure the last bit is a zero to force unsigned numbers *) + let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);; let to_vec_inc len (V_lit(L_aux (L_num n) ln)) = @@ -61,8 +62,9 @@ let function_map = [ ("eq", eq); ("vec_concat", vec_concat); ("is_one", is_one); - ("to_num_inc", to_num_inc); - ("to_num_dec", to_num_dec); + ("to_num_inc", to_num false); + ("to_num_dec", to_num false); + ("exts", to_num true); (* XXX the size of the target vector should be given by the interpreter *) ("to_vec_inc", to_vec_inc 64); ("to_vec_dec", to_vec_dec 64); diff --git a/src/test/power.sail b/src/test/power.sail index 68416bfc..704fc475 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -1,6 +1,7 @@ -(* XXX sign extension --- this should really be vector -> int, with - negative integers allowed *) -function forall Type 'a . 'a exts ( x ) = x +(* XXX sign extension --- note that this produces a signed integer, + the constraints on the range of the result is TODO *) +val extern forall Nat 'n. bit['n] -> nat effect pure exts + (* XXX binary coded decimal *) function forall Type 'a . 'a dec_to_bcd ( x ) = x function forall Type 'a . 'a bcd_to_dec ( x ) = x |