From 8859f8b1f4d17dfeaac878527ad0b1bb1610cef7 Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Sun, 28 Apr 2024 15:30:12 +0200 Subject: [PATCH] Fix inconsistent use of __div__ and __truediv__ --- src/nagini_translation/lib/constants.py | 18 ++++++++++-------- src/nagini_translation/resources/bool.sil | 2 +- src/nagini_translation/resources/float.sil | 8 ++++---- .../resources/float_ieee32.sil | 4 ++-- .../resources/float_real.sil | 4 ++-- .../resources/preamble.index | 10 +++++----- .../sif/resources/preamble.index | 6 +++--- 7 files changed, 27 insertions(+), 25 deletions(-) diff --git a/src/nagini_translation/lib/constants.py b/src/nagini_translation/lib/constants.py index 40f43349..731a7203 100644 --- a/src/nagini_translation/lib/constants.py +++ b/src/nagini_translation/lib/constants.py @@ -218,13 +218,10 @@ '__add__', '__sub__', '__mul__', + '__matmul__', '__truediv__', '__floordiv__', '__mod__', - '__neg__', - '__pos__', - '__invert__', - '__divmod__', '__pow__', '__lshift__', @@ -232,6 +229,11 @@ '__and__', '__or__', '__xor__', + + '__neg__', + '__pos__', + '__invert__', + '__radd__', '__rsub__', @@ -262,7 +264,7 @@ '__isub__', '__imul__', '__imatmul__', - '__idiv__', + '__itruediv__', '__ifloordiv__', '__imod__', '__ipow__', @@ -378,7 +380,7 @@ ast.Sub: '__sub__', ast.Mult: '__mul__', ast.MatMult: '__matmul__', - ast.Div: '__div__', + ast.Div: '__truediv__', ast.FloorDiv: '__floordiv__', ast.Mod: '__mod__', ast.Pow: '__pow__', @@ -394,7 +396,7 @@ ast.Sub: '__isub__', ast.Mult: '__imul__', ast.MatMult: '__imatmul__', - ast.Div: '__idiv__', + ast.Div: '__itruediv__', ast.FloorDiv: '__ifloordiv__', ast.Mod: '__imod__', ast.Pow: '__ipow__', @@ -410,7 +412,7 @@ ast.Sub: '__rsub__', ast.Mult: '__rmul__', ast.MatMult: '__rmatmul__', - ast.Div: '__rdiv__', + ast.Div: '__rtruediv__', ast.FloorDiv: '__rfloordiv__', ast.Mod: '__rmod__', ast.Pow: '__rpow__', diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil index 34e1bcc7..31451380 100644 --- a/src/nagini_translation/resources/bool.sil +++ b/src/nagini_translation/resources/bool.sil @@ -133,7 +133,7 @@ function int___floordiv__(self: Int, other: Int): Int self \ other } -function int___div__(self: Int, other: Int): Ref +function int___truediv__(self: Int, other: Int): Ref decreases _ requires @error("Divisor may be zero.")(other != 0) ensures (self % other == 0) ==> (typeof(result) == int() && int___unbox__(result) == self \ other) diff --git a/src/nagini_translation/resources/float.sil b/src/nagini_translation/resources/float.sil index 37b708e0..1b00c130 100644 --- a/src/nagini_translation/resources/float.sil +++ b/src/nagini_translation/resources/float.sil @@ -92,7 +92,7 @@ function float___rmul__(self: Ref, other: Ref): Ref ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> (result == __prim__int___box__(int___mul__(int___unbox__(other), int___unbox__(self)))) -function float___div__(self: Ref, other: Ref): Ref +function float___truediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) @@ -100,7 +100,7 @@ function float___div__(self: Ref, other: Ref): Ref requires issubtype(typeof(other), int()) // cannot express non-zero at the moment ensures issubtype(typeof(result), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> - (result == int___div__(int___unbox__(self), int___unbox__(other))) + (result == int___truediv__(int___unbox__(self), int___unbox__(other))) function float___pos__(self: Ref): Ref decreases _ @@ -114,7 +114,7 @@ function float___neg__(self: Ref): Ref ensures issubtype(typeof(result), float()) ensures issubtype(typeof(self), int()) ==> result == int___neg__(self) -function float___rdiv__(self: Ref, other: Ref): Ref +function float___rtruediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) @@ -122,7 +122,7 @@ function float___rdiv__(self: Ref, other: Ref): Ref requires issubtype(typeof(self), int()) // cannot express non-zero at the moment ensures issubtype(typeof(result), float()) ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==> - (result == int___div__(int___unbox__(other), int___unbox__(self))) + (result == int___truediv__(int___unbox__(other), int___unbox__(self))) function float___int__(self: Ref): Ref decreases _ diff --git a/src/nagini_translation/resources/float_ieee32.sil b/src/nagini_translation/resources/float_ieee32.sil index aa436927..68327fe6 100644 --- a/src/nagini_translation/resources/float_ieee32.sil +++ b/src/nagini_translation/resources/float_ieee32.sil @@ -90,7 +90,7 @@ function float___rmul__(self: Ref, other: Ref): Ref ensures issubtype(typeof(result), float()) ensures result == __prim__perm___box__(___float32_mul(float___unbox__(other), float___unbox__(self))) -function float___div__(self: Ref, other: Ref): Ref +function float___truediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) @@ -110,7 +110,7 @@ function float___neg__(self: Ref): Ref ensures issubtype(typeof(result), float()) ensures result == __prim__perm___box__(___float32_neg(float___unbox__(self))) -function float___rdiv__(self: Ref, other: Ref): Ref +function float___rtruediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) diff --git a/src/nagini_translation/resources/float_real.sil b/src/nagini_translation/resources/float_real.sil index 2722a54b..e0377b1e 100644 --- a/src/nagini_translation/resources/float_real.sil +++ b/src/nagini_translation/resources/float_real.sil @@ -90,7 +90,7 @@ function float___rmul__(self: Ref, other: Ref): Ref ensures issubtype(typeof(result), float()) ensures result == __prim__perm___box__(float___unbox__(other) * float___unbox__(self)) -function float___div__(self: Ref, other: Ref): Ref +function float___truediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) @@ -109,7 +109,7 @@ function float___neg__(self: Ref): Ref ensures issubtype(typeof(result), float()) ensures result == __prim__perm___box__(-float___unbox__(self)) -function float___rdiv__(self: Ref, other: Ref): Ref +function float___rtruediv__(self: Ref, other: Ref): Ref decreases _ requires issubtype(typeof(self), float()) requires issubtype(typeof(other), float()) diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index index 353a360f..15bd1438 100644 --- a/src/nagini_translation/resources/preamble.index +++ b/src/nagini_translation/resources/preamble.index @@ -241,7 +241,7 @@ "args": ["__prim__int", "__prim__int"], "type": "__prim__int" }, - "__div__": { + "__truediv__": { "args": ["__prim__int", "__prim__int"], "type": "float" }, @@ -346,15 +346,15 @@ "type": "float", "requires": ["int___mul__", "int___unbox__", "unbox", "__prim__perm___box__"] }, - "__div__": { + "__truediv__": { "args": ["float", "float"], "type": "float", - "requires": ["int___div__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"] + "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"] }, - "__rdiv__": { + "__rtruediv__": { "args": ["float", "float"], "type": "float", - "requires": ["int___div__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"] + "requires": ["int___truediv__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"] }, "__ge__": { "args": ["float", "float"], diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index index b1c601d8..9e6bfd42 100644 --- a/src/nagini_translation/sif/resources/preamble.index +++ b/src/nagini_translation/sif/resources/preamble.index @@ -244,7 +244,7 @@ "args": ["__prim__int", "__prim__int"], "type": "__prim__int" }, - "__div__": { + "__truediv__": { "args": ["__prim__int", "__prim__int"], "type": "float" }, @@ -328,10 +328,10 @@ "type": "float", "requires": ["int___mul__", "int___unbox__"] }, - "__div__": { + "__truediv__": { "args": ["float", "float"], "type": "float", - "requires": ["int___div__", "int___unbox__"] + "requires": ["int___truediv__", "int___unbox__"] }, "__ge__": { "args": ["float", "float"],