Use fully qualified type names

.vscode/launch.json

@@ -0,0 +1,16 @@
+{
+    // Use IntelliSense to learn about possible attributes.
+    // Hover to view descriptions of existing attributes.
+    // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
+    "version": "0.2.0",
+    "configurations": [
+        {
+            "name": "Python: Current File",
+            "type": "python",
+            "request": "launch",
+            "program": "${file}",
+            "console": "integratedTerminal",
+            "justMyCode": true
+        }
+    ]
+}

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+  "python.testing.pytestArgs": ["tests"],
+  "python.testing.unittestEnabled": false,
+  "python.testing.pytestEnabled": true
+}

rflx/generator/session.py

@@ -238,11 +238,11 @@ def _ada_type(self, identifier: rid.ID) -> ID:
         if model.is_builtin_type(identifier):
             return ID(identifier.name)
 
-        return ID(model.qualified_type_identifier(identifier, self._session.package))
+        return ID(model.internal_type_identifier(identifier, self._session.package))
 
     def _model_type(self, identifier: rid.ID) -> model.Type:
         return self._session.types[
-            model.qualified_type_identifier(identifier, self._session.package)
+            model.internal_type_identifier(identifier, self._session.package)
         ]
 
     def _create(self) -> None:

rflx/model/__init__.py

@@ -36,7 +36,7 @@
     Scalar as Scalar,
     Sequence as Sequence,
     Type as Type,
+    internal_type_identifier as internal_type_identifier,
     is_builtin_type as is_builtin_type,
     is_internal_type as is_internal_type,
-    qualified_type_identifier as qualified_type_identifier,
 )

rflx/model/message.py

@@ -187,38 +187,41 @@ def __str__(self) -> str:
 
         parameters = "; ".join(
             [
-                f"{p.identifier} : {type_identifier}"
-                for p, t in self.parameter_types.items()
-                for type_identifier in (
-                    t.name if mty.is_builtin_type(t.identifier) else t.identifier,
-                )
+                f"{parameter_field.identifier} : {parameter_type_identifier}"
+                for parameter_field, parameter_type in self.parameter_types.items()
+                for parameter_type_identifier in (parameter_type.qualified_identifier,)
             ]
         )
         if parameters:
             parameters = f" ({parameters})"
 
         fields = ""
         field_list = [INITIAL, *self.fields]
-        for i, f in enumerate(field_list):
-            if f != INITIAL:
+        for i, field in enumerate(field_list):
+            if field != INITIAL:
                 fields += "\n" if fields else ""
-                fields += f"{f.name} : {self.types[f].name}"
-            outgoing = self.outgoing(f)
+                field_type_identifier = self.types[field].qualified_identifier
+                fields += f"{field.name} : {field_type_identifier}"
+            outgoing = self.outgoing(field)
             if not (
                 len(outgoing) == 1
                 and outgoing[0].condition == expr.TRUE
                 and outgoing[0].size == expr.UNDEFINED
                 and outgoing[0].first == expr.UNDEFINED
                 and (i >= len(field_list) - 1 or field_list[i + 1] == outgoing[0].target)
             ):
-                if f == INITIAL:
+                if field == INITIAL:
                     fields += "null"
                 fields += "\n" + indent("\n".join(str(o) for o in outgoing), 3)
             if fields:
                 fields += ";"
 
         return f"type {self.name}{parameters} is\n   message\n{indent(fields, 6)}\n   end message"
 
+    @property
+    def direct_dependencies(self) -> List[mty.Type]:
+        return [self, *self.__types.values()]
+
     @property
     def dependencies(self) -> List[mty.Type]:
         return [self, *unique(a for t in self.__types.values() for a in t.dependencies)]

rflx/model/model.py

@@ -1,11 +1,11 @@
-from itertools import groupby
 from pathlib import Path
 from typing import Dict, Sequence
 
 from rflx import const
-from rflx.common import Base, indent, verbose_repr
+from rflx.common import Base, verbose_repr
 from rflx.error import RecordFluxError, Severity, Subsystem
 from rflx.identifier import ID
+from rflx.model.package import Package
 
 from . import message, session, type_
 
@@ -42,29 +42,26 @@ def sessions(self) -> Sequence[session.Session]:
         return self.__sessions
 
     def create_specifications(self) -> Dict[ID, str]:
-        return {
-            package: f"package {package} is\n\n"
-            + indent("\n\n".join(f"{d};" for d in declarations), 3)
-            + f"\n\nend {package};"
-            for package, declarations in groupby(
-                [
-                    *[
-                        t
-                        for t in self.__types
-                        if not type_.is_builtin_type(t.name) and not type_.is_internal_type(t.name)
-                    ],
-                    *self.__sessions,
-                ],
-                lambda x: x.package,
-            )
-        }
+        pkgs: Dict[ID, Package] = {}
+        for ty in self.__types:
+            if not type_.is_builtin_type(ty.name) and not type_.is_internal_type(ty.name):
+                pkg_name: ID = ty.package
+                pkg: Package = pkgs.setdefault(pkg_name, Package(pkg_name))
+                for dep in ty.direct_dependencies:
+                    if dep.package not in [
+                        pkg_name,
+                        const.BUILTINS_PACKAGE,
+                        const.INTERNAL_PACKAGE,
+                    ]:
+                        pkg.imports.append(dep.package)
+                pkg.types.append(ty)
+        for sess in self.__sessions:
+            pkg_name = sess.package
+            pkgs.setdefault(pkg_name, Package(pkg_name)).sessions.append(sess)
+        return {id: str(pkg) for id, pkg in pkgs.items()}
 
     def write_specification_files(self, output_dir: Path) -> None:
-        """
-        Write corresponding specification files into given directory.
-
-        Limitation: Potentially necessary with-clauses are not generated.
-        """
+        """Write corresponding specification files (one per package) into given directory."""
         for package, specification in self.create_specifications().items():
             (output_dir / f"{package.flat.lower()}.rflx").write_text(specification)
 

rflx/model/package.py

@@ -0,0 +1,41 @@
+import textwrap
+from dataclasses import dataclass, field
+from typing import List
+
+from rflx.identifier import ID
+
+from . import session, type_
+
+
+@dataclass
+class Package:
+    name: ID
+    imports: List[ID] = field(default_factory=list)
+    types: List[type_.Type] = field(default_factory=list)
+    sessions: List[session.Session] = field(default_factory=list)
+
+    @property
+    def imports_str(self) -> str:
+        return "\n".join(f"with {i};" for i in self.imports)
+
+    @property
+    def begin_str(self) -> str:
+        return f"package {self.name} is"
+
+    @property
+    def end_str(self) -> str:
+        return f"end {self.name};"
+
+    @property
+    def types_str(self) -> str:
+        raw = "\n\n".join(f"{t};" for t in self.types)
+        return textwrap.indent(raw, " " * 3)
+
+    @property
+    def sessions_str(self) -> str:
+        raw = "\n\n".join(f"{s};" for s in self.sessions)
+        return textwrap.indent(raw, " " * 3)
+
+    def __str__(self) -> str:
+        pieces = [self.imports_str, self.begin_str, self.types_str, self.sessions_str, self.end_str]
+        return "\n\n".join(filter(None, pieces))

rflx/model/session.py

@@ -416,15 +416,15 @@ def undefined_type(type_identifier: StrID, location: Optional[Location]) -> None
             self.__reference_variable_declaration(d.variables(), visible_declarations)
 
             if isinstance(d, decl.TypeDeclaration):
-                type_identifier = mty.qualified_type_identifier(k, self.package)
+                type_identifier = mty.internal_type_identifier(k, self.package)
                 if type_identifier in self.types:
                     self.error.extend(
                         [(f'type "{k}" shadows type', Subsystem.MODEL, Severity.ERROR, d.location)],
                     )
                 self.types[type_identifier] = d.type_definition
 
             elif isinstance(d, decl.TypeCheckableDeclaration):
-                type_identifier = mty.qualified_type_identifier(d.type_identifier, self.package)
+                type_identifier = mty.internal_type_identifier(d.type_identifier, self.package)
                 if type_identifier in self.types:
                     self.error.extend(
                         d.check_type(
@@ -438,7 +438,7 @@ def undefined_type(type_identifier: StrID, location: Optional[Location]) -> None
 
                 if isinstance(d, decl.FunctionDeclaration):
                     for a in d.arguments:
-                        type_identifier = mty.qualified_type_identifier(
+                        type_identifier = mty.internal_type_identifier(
                             a.type_identifier, self.package
                         )
                         if type_identifier in self.types:
@@ -643,7 +643,7 @@ def __typify_variable(
                         if isinstance(t, Refinement) and t.sdu.identifier == identifier
                     ]
             if isinstance(expression, expr.MessageAggregate):
-                type_identifier = mty.qualified_type_identifier(identifier, self.package)
+                type_identifier = mty.internal_type_identifier(identifier, self.package)
                 if type_identifier in self.types:
                     expression.type_ = self.types[type_identifier].type_
 

rflx/model/type_.py

@@ -16,6 +16,16 @@ class Type(BasicDeclaration):
     def type_(self) -> rty.Type:
         return rty.Undefined()
 
+    @property
+    def direct_dependencies(self) -> ty.List["Type"]:
+        """
+        Return a list consisting of the type and all the types on which the type directly depends.
+
+        The dependencies are not determined recursively, i.e. the dependencies
+        of dependencies are not considered.
+        """
+        return [self]
+
     @property
     def dependencies(self) -> ty.List["Type"]:
         """
@@ -25,6 +35,22 @@ def dependencies(self) -> ty.List["Type"]:
         """
         return [self]
 
+    @property
+    def qualified_identifier(self) -> ID:
+        """
+        Return the qualified identifier of this type.
+
+        The qualified identifier of a type is defined as its complete package
+        path followed by the type name, or just the type name if the type is
+        builtin or internal.
+        """
+        identifier = self.identifier
+        return (
+            ID(self.name, location=identifier.location)
+            if is_builtin_type(identifier) or is_internal_type(identifier)
+            else identifier
+        )
+
 
 class Scalar(Type):
     def __init__(self, identifier: StrID, size: expr.Expr, location: Location = None) -> None:
@@ -591,7 +617,7 @@ def __repr__(self) -> str:
         return verbose_repr(self, ["identifier", "element_type"])
 
     def __str__(self) -> str:
-        return f"type {self.name} is sequence of {self.element_type.name}"
+        return f"type {self.name} is sequence of {self.element_type.qualified_identifier}"
 
     @property
     def type_(self) -> rty.Type:
@@ -601,6 +627,10 @@ def type_(self) -> rty.Type:
     def element_size(self) -> expr.Expr:
         return expr.Size(self.element_type.name)
 
+    @property
+    def direct_dependencies(self) -> ty.List["Type"]:
+        return [self, self.element_type]
+
     @property
     def dependencies(self) -> ty.List["Type"]:
         return [self, *self.element_type.dependencies]
@@ -676,7 +706,14 @@ def is_builtin_type(identifier: StrID) -> bool:
     )
 
 
-def qualified_type_identifier(identifier: ID, package: ID = None) -> ID:
+def internal_type_identifier(identifier: ID, package: ID = None) -> ID:
+    """
+    Return the internal identifier of a type.
+
+    The internal identifier is defined as its complete package path
+    (`__BUILTINS__` for builtin types, and `__INTERNAL__` for internal types)
+    followed by the type name.
+    """
     if is_builtin_type(identifier):
         return ID(const.BUILTINS_PACKAGE * identifier.name, location=identifier.location)