Fixed type inference for float literals, added some Viper-level depen…

…dencies
marcoeilers · Dec 6, 2023 · bcf5ec7 · bcf5ec7
1 parent f3ee12f
commit bcf5ec7
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/src/nagini_translation/lib/resolver.py b/src/nagini_translation/lib/resolver.py
@@ -13,6 +13,7 @@
     BUILTINS,
     BYTES_TYPE,
     DICT_TYPE,
+    FLOAT_TYPE,
     INT_TYPE,
     LIST_TYPE,
     OBJECT_TYPE,
@@ -261,7 +262,10 @@ def _do_get_type(node: ast.AST, containers: List[ContainerInterface],
         # the node refers to something unknown in the given context.
         return None
     if isinstance(node, ast.Num):
-        return module.global_module.classes[INT_TYPE]
+        if isinstance(node.n, int):
+            return module.global_module.classes[INT_TYPE]
+        if isinstance(node.n, float):
+            return module.global_module.classes[FLOAT_TYPE]
     elif isinstance(node, ast.Tuple):
         args = [get_type(arg, containers, container) for arg in node.elts]
         return GenericType(module.global_module.classes[TUPLE_TYPE],

diff --git a/src/nagini_translation/resources/preamble.index b/src/nagini_translation/resources/preamble.index
@@ -280,7 +280,8 @@
     "functions": {
         "__create__": {
             "args": ["__prim__int"],
-            "type": "float"
+            "type": "float",
+            "requires": ["__prim__perm___box__"]
         },
         "__unbox__": {
             "args": ["float"],
@@ -290,7 +291,7 @@
         "__bool__": {
             "args": ["float"],
             "type": "__prim__bool",
-            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___bool__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
         },
         "__eq__": {
             "args": ["float", "object"],
@@ -315,7 +316,7 @@
         "__div__": {
             "args": ["float", "float"],
             "type": "float",
-            "requires": ["int___div__", "int___unbox__", "unbox", "__prim__perm___box__"]
+            "requires": ["int___div__", "int___unbox__", "unbox", "__prim__perm___box__", "___float32_zero"]
         },
         "__ge__": {
             "args": ["float", "float"],