diff --git a/cryptol-remote-api/python/cryptol/bitvector.py b/cryptol-remote-api/python/cryptol/bitvector.py index ec9e3111b..6155217f1 100644 --- a/cryptol-remote-api/python/cryptol/bitvector.py +++ b/cryptol-remote-api/python/cryptol/bitvector.py @@ -149,7 +149,7 @@ def to_int(self) -> int: def to_signed_int(self) -> int: """Return the signed (i.e., two's complement) integer the ``BV`` represents.""" - if not self.msb(): + if self.__size == 0 or not self.msb(): n = self.__value else: n = 0 - ((2 ** self.__size) - self.__value) diff --git a/cryptol-remote-api/python/cryptol/quoting.py b/cryptol-remote-api/python/cryptol/quoting.py index 7503c87ff..9cb6e75ab 100644 --- a/cryptol-remote-api/python/cryptol/quoting.py +++ b/cryptol-remote-api/python/cryptol/quoting.py @@ -14,6 +14,8 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str: if isinstance(val, bool): return 'True' if val else 'False' elif isinstance(val, tuple): + if len(val) == 1: + raise TypeError("Unable to convert 1-tuple to Cryptol syntax: " + str(val)) return '(' + ', '.join(to_cryptol_str(x) for x in val) + ')' elif isinstance(val, dict): return '{' + ', '.join(f'{k} = {to_cryptol_str(v)}' for k,v in val.items()) + '}' @@ -22,14 +24,15 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str: elif isinstance(val, list): return '[' + ', '.join(to_cryptol_str(x) for x in val) + ']' elif isinstance(val, BV): - if val.size() % 4 == 0: + if val.size() > 0 and val.size() % 4 == 0: return val.hex() else: return f'({val.to_signed_int()} : [{val.size()}])' elif isinstance(val, OpaqueValue): return str(val) elif isinstance(val, str): - return f'"{val}"' + chars = list(val.encode('latin-1')) + return f'({to_cryptol_str(chars)} : [{len(chars)}][8])' elif hasattr(val, '__to_cryptol_str__'): return parenthesize(val.__to_cryptol_str__()) else: diff --git a/cryptol-remote-api/python/tests/cryptol/test_quoting.py b/cryptol-remote-api/python/tests/cryptol/test_quoting.py index 64508c1a1..dd6fbac56 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_quoting.py +++ b/cryptol-remote-api/python/tests/cryptol/test_quoting.py @@ -24,15 +24,26 @@ def test_quoting(self): self.assertEqual(cry_f('id {BV(size=7, value=1)}'), cry('id (1 : [7])')) self.assertEqual(cry_eval_f('id {BV(size=7, value=1)}'), BV(size=7, value=1)) + self.assertEqual(cry_f('id {BV(size=0, value=0)}'), cry('id (0 : [0])')) + self.assertEqual(cry_eval_f('id {BV(size=0, value=0)}'), BV(size=0, value=0)) self.assertEqual(cry_f('{ {"a": x, "b": x} }'), cry('{a = 0x01, b = 0x01}')) self.assertEqual(cry_f('{{a = {x}, b = {x}}}'), cry('{a = 0x01, b = 0x01}')) + with self.assertRaises(TypeError): + cry_f('{(0,)}') # Cryptol does not have 1-tuples + self.assertEqual(cry_f('id {5}'), cry('id 5')) - self.assertEqual(cry_f('id {5!s}'), cry('id "5"')) - self.assertEqual(cry_f('id {5:#x}'), cry('id "0x5"')) + self.assertEqual(cry_f('id {5!s}'), cry('id ([53] : [1][8])')) # id "5" + self.assertEqual(cry_f('id {5:#x}'), cry('id ([48, 120, 53] : [3][8])')) # id "0x5" self.assertEqual(cry_f('id {BV(4,5)}'), cry('id 0x5')) + s = '" \n ÿ \\' + self.assertEqual(cry_f('{s}'), cry('([34, 32, 10, 32, 255, 32, 92] : [7][8])')) # "\" \n ÿ \\" + self.assertEqual(cry_eval_f('{s}'), [BV(8,c) for c in [34, 32, 10, 32, 255, 32, 92]]) + with self.assertRaises(UnicodeEncodeError): + cry_f('{"π"}') # 'latin-1' codec can't encode character (960 >= 256) + # Only here to check backwards compatability, the above syntax is preferred y = cry('g')(cry_f('{x}')) z = cry('h')(cry_f('{y}'))