Making types ordinary objects that can be stored e.g. in tuples

src/nagini_translation/lib/constants.py

@@ -311,6 +311,8 @@
 
 BOOL_TYPE = 'bool'
 
+TYPE_TYPE = 'type'
+
 PRIMITIVE_PREFIX = '__prim__'
 
 PRIMITIVE_INT_TYPE = PRIMITIVE_PREFIX + INT_TYPE
@@ -325,13 +327,15 @@
 
 PRIMITIVE_MSET_TYPE = PRIMITIVE_PREFIX + 'Multiset'
 
+PRIMITIVE_TYPE_TYPE = 'PyType'
+
 
 OBJECT_TYPE = 'object'
 
 CALLABLE_TYPE = 'Callable'
 
 PRIMITIVES = {PRIMITIVE_INT_TYPE, PRIMITIVE_BOOL_TYPE, PRIMITIVE_SEQ_TYPE,
-              PRIMITIVE_SET_TYPE, CALLABLE_TYPE, PRIMITIVE_MSET_TYPE}
+              PRIMITIVE_SET_TYPE, CALLABLE_TYPE, PRIMITIVE_MSET_TYPE, PRIMITIVE_TYPE_TYPE}
 
 BOXED_PRIMITIVES = {INT_TYPE, BOOL_TYPE}
 

src/nagini_translation/lib/program_nodes.py

@@ -1,5 +1,5 @@
 """
-Copyright (c) 2019 ETH Zurich
+Copyright (c) 2025 ETH Zurich
 This Source Code Form is subject to the terms of the Mozilla Public
 License, v. 2.0. If a copy of the MPL was not distributed with this
 file, You can obtain one at http://mozilla.org/MPL/2.0/.
@@ -24,6 +24,7 @@
     PRIMITIVE_PREFIX,
     PRIMITIVE_SEQ_TYPE,
     PRIMITIVE_SET_TYPE,
+    PRIMITIVE_TYPE_TYPE,
     PRIMITIVES,
     PSEQ_TYPE,
     PSET_TYPE,
@@ -707,10 +708,12 @@ def try_box(self) -> 'PythonClass':
             boxed_name = self.name[len(PRIMITIVE_PREFIX):]
             if boxed_name == 'Set':
                 boxed_name = PSET_TYPE
-            if boxed_name == 'Multiset':
+            elif boxed_name == 'Multiset':
                 boxed_name = PMSET_TYPE
-            if boxed_name == 'Seq':
+            elif boxed_name == 'Seq':
                 boxed_name = PSEQ_TYPE
+            elif self.name == PRIMITIVE_TYPE_TYPE:
+                boxed_name = 'type'
             return self.module.classes[boxed_name]
         return self
 

src/nagini_translation/lib/resolver.py

@@ -26,6 +26,7 @@
     SET_TYPE,
     STRING_TYPE,
     TUPLE_TYPE,
+    TYPE_TYPE,
 )
 from nagini_translation.lib.program_nodes import (
     ContainerInterface,
@@ -76,15 +77,19 @@ def get_target(node: ast.AST,
         if (container and func_name == 'Result' and
                 isinstance(container, PythonMethod)):
             # In this case the immediate container must be a method, and we
-            # return its result type
-            return container.type
+            return None
         elif (container and func_name == 'super' and
                   isinstance(container, PythonMethod)):
             # Return the type of the current method's superclass
             return container.cls.superclass
         elif func_name == 'cast':
             return None
-        return get_target(node.func, containers, container)
+        func_target = get_target(node.func, containers, container)
+        if isinstance(func_target, PythonType):
+            # this is a constructor call, it's not pointing at an actual PythonNode
+            return None
+        else:
+            return func_target
     elif isinstance(node, ast.Attribute):
         # Find the type of the LHS, so that we can look through its members.
         lhs = get_type(node.value, containers, container)
@@ -99,6 +104,8 @@ def get_target(node: ast.AST,
             # defined in the class. So instead of type[C], we want to look in
             # class C directly here.
             lhs = lhs.type_args[0]
+        if isinstance(lhs, PythonClass) and lhs.name == TYPE_TYPE:
+            lhs = get_target(node.value, containers, container)
         if isinstance(lhs, GenericType):
             # Use the class, since we want to look for members.
             lhs = lhs.cls
@@ -258,7 +265,7 @@ def _do_get_type(node: ast.AST, containers: List[ContainerInterface],
                 else:
                     error = 'generic.constructor.without.type'
                     raise InvalidProgramException(node, error)
-            return target
+            return module.global_module.classes[TYPE_TYPE]
     if isinstance(node, (ast.Attribute, ast.Name)):
         if isinstance(node, ast.Attribute):
             lhs = _do_get_type(node.value, containers, container)
@@ -422,6 +429,45 @@ def _get_call_type(node: ast.Call, module: PythonModule,
                    current_function: PythonMethod,
                    containers: List[ContainerInterface],
                    container: PythonNode) -> PythonType:
+    call_target = get_target(node.func, containers, container)
+    if isinstance(call_target, PythonMethod):
+        if isinstance(node.func, ast.Attribute):
+            rec_target = get_target(node.func.value, containers, container)
+            if not isinstance(rec_target, PythonModule):
+                rectype = get_type(node.func.value, containers, container)
+                if call_target.generic_type != -1:
+                    if call_target.generic_type == -2:
+                        return rectype
+                    return rectype.type_args[call_target.generic_type]
+                if isinstance(call_target.type, TypeVar):
+                    while rectype.python_class is not call_target.cls:
+                        rectype = rectype.superclass
+                    name_list = list(rectype.python_class.type_vars.keys())
+                    index = name_list.index(call_target.type.name)
+                    return rectype.type_args[index]
+    if (isinstance(call_target, PythonClass) and
+            call_target.type_vars):
+        # This is a call to a constructor of a generic class; it's not
+        # enough to just return the class, we need the entire type with
+        # type arguments. We only support that if we can get it directly
+        # from mypy, i.e., when the result is assigned to a variable
+        # and we can get the variable type.
+        if hasattr(node, '_parent') and node._parent and isinstance(node._parent, (ast.Assign, ast.AnnAssign)):
+            trgt = node._parent.targets[0] if isinstance(node._parent, ast.Assign) else node._parent.target
+            ann_type = get_type(trgt, containers, container)
+            if isinstance(ann_type, GenericType) and ann_type.python_class == call_target:
+                return ann_type
+        if (call_target.name in (PSEQ_TYPE, PSET_TYPE, PMSET_TYPE) and
+                isinstance(node, ast.Call) and node.args):
+            arg_types = [get_type(arg, containers, container)
+                         for arg in node.args]
+            return GenericType(call_target, [common_supertype(arg_types)])
+        else:
+            error = 'generic.constructor.without.type'
+            raise InvalidProgramException(node, error)
+    if isinstance(call_target, PythonType):
+        # constructor call
+        return call_target
     func_name = get_func_name(node)
     if func_name == 'super':
         if len(node.args) == 2:
@@ -511,7 +557,7 @@ def _get_call_type(node: ast.Call, module: PythonModule,
             else:
                 raise UnsupportedException(node)
         if node.func.id in module.classes:
-            return module.global_module.classes[node.func.id]
+            return module.classes[node.func.id]
         elif module.get_func_or_method(node.func.id) is not None:
             target = module.get_func_or_method(node.func.id)
             return target.type

src/nagini_translation/resources/bool.sil

@@ -391,3 +391,19 @@ domain __SumHelper[T$] {
         forall __ss1: Seq[Int], __ss2: Seq[Int] :: { __sum(__ss1), __sum(__ss2) } __toMS(__ss1) == __toMS(__ss2) ==> __sum(__ss1) == __sum(__ss2)
     }
 }
+
+function PyType___box__(prim: PyType): Ref
+    decreases _
+    ensures typeof(result) == type()
+    ensures type___unbox__(result) == prim
+
+function type___unbox__(box: Ref): PyType
+    decreases _
+    requires issubtype(typeof(box), type())
+    ensures PyType___box__(result) == box
+
+function type___eq__(self: Ref, other: Ref): Bool
+    decreases _
+    requires issubtype(typeof(self), type())
+    requires issubtype(typeof(other), type())
+    ensures result == (type___unbox__(self) == type___unbox__(other))

src/nagini_translation/resources/builtins.json

@@ -14,7 +14,7 @@
             "type": "str"
         },
         "__cast__": {
-            "args": ["type", "object"],
+            "args": ["PyType", "object"],
             "type": "object"
         }
     }
@@ -559,27 +559,27 @@
             "type": "tuple"
         },
         "__create1__": {
-            "args": ["object", "type", "__prim__int"],
+            "args": ["object", "PyType", "__prim__int"],
             "type": "tuple"
         },
         "__create2__": {
-            "args": ["object", "object", "type", "type", "__prim__int"],
+            "args": ["object", "object", "PyType", "PyType", "__prim__int"],
             "type": "tuple"
         },
         "__create3__": {
-            "args": ["object", "object", "object", "type", "type", "type", "__prim__int"],
+            "args": ["object", "object", "object", "PyType", "PyType", "PyType", "__prim__int"],
             "type": "tuple"
         },
         "__create4__": {
-            "args": ["object", "object", "object", "object", "type", "type", "type", "type", "__prim__int"],
+            "args": ["object", "object", "object", "object", "PyType", "PyType", "PyType", "PyType", "__prim__int"],
             "type": "tuple"
         },
         "__create5__": {
-            "args": ["object", "object", "object", "object", "object", "type", "type", "type", "type", "type", "__prim__int"],
+            "args": ["object", "object", "object", "object", "object", "PyType", "PyType", "PyType", "PyType", "PyType", "__prim__int"],
             "type": "tuple"
         },
         "__create6__": {
-            "args": ["object", "object", "object", "object", "object", "object", "type", "type", "type", "type", "type", "type", "__prim__int"],
+            "args": ["object", "object", "object", "object", "object", "object", "PyType", "PyType", "PyType", "PyType", "PyType", "PyType", "__prim__int"],
             "type": "tuple"
         },
         "__getitem__": {
@@ -642,10 +642,34 @@
 "__prim__Seq": {},
 "__prim__Set": {},
 "__prim__Multiset": {},
+"PyType": {
+    "functions": {
+        "__box__": {
+            "args": ["PyType"],
+            "type": "type",
+            "requires": ["type___unbox__"]
+        }
+    }
+},
+"type": {
+    "functions": {
+        "__unbox__": {
+            "args": ["type"],
+            "type": "PyType",
+            "requires": ["PyType___box__"]
+        },
+        "__eq__": {
+            "args": ["type", "object"],
+            "type": "__prim__bool",
+            "requires": ["__unbox__"]
+        }
+    },
+    "extends": "object"
+},
 "PSeq": {
     "functions": {
         "__create__": {
-            "args": ["__prim__Seq", "type"],
+            "args": ["__prim__Seq", "PyType"],
             "type": "PSeq"
         },
         "__unbox__": {
@@ -697,7 +721,7 @@
 "PSet": {
     "functions": {
         "__create__": {
-            "args": ["__prim__Set", "type"],
+            "args": ["__prim__Set", "PyType"],
             "type": "PSet"
         },
         "__unbox__": {
@@ -735,7 +759,7 @@
 "PMultiset": {
     "functions": {
         "__create__": {
-            "args": ["__prim__Multiset", "type"],
+            "args": ["__prim__Multiset", "PyType"],
             "type": "PMultiset"
         },
         "__unbox__": {
@@ -873,9 +897,6 @@
 },
 "LevelType": {
 },
-"type": {
-    "extends": "object"
-},
 "Callable": {
     "extends": "object"
 },

src/nagini_translation/resources/pytype.sil

@@ -40,4 +40,5 @@ domain PyType {
     unique function str(): PyType
     unique function object(): PyType
     unique function NoneType(): PyType
+    unique function type(): PyType
 }

src/nagini_translation/translators/abstract.py

@@ -351,6 +351,9 @@ def type_check(self, lhs: Expr, type: PythonType,
         return self.config.type_translator.type_check(
             lhs, type, position, ctx, inhale_exhale=inhale_exhale)
 
+    def subtype_check(self, obj: Expr, type_expr: Expr, position: 'silver.ast.Position', ctx: Context) -> Expr:
+        return self.config.type_translator.subtype_check(obj, type_expr, position, ctx)
+
     def bind_type_vars(self, method: PythonMethod, ctx: Context) -> None:
         return self.config.method_translator.bind_type_vars(method, ctx)