Consistent and readable generics

doc/source/doc/parametric_models.md

@@ -41,7 +41,7 @@ In order to obtain a standard DTMC, MDP or other Markov model, we need to instan
 ```{code-cell} python3
 import stormpy.pars
 
-instantiator = stormpy.pars.PDtmcInstantiator(model)
+instantiator = stormpy.pars.ModelInstantiator[stormpy.ModelType.DTMC, float](model)
 ```
 
 Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows:

examples/parametric_models/01-parametric-models.py

@@ -16,7 +16,7 @@ def example_parametric_models_01():
     parameters = model.collect_all_parameters()
     assert len(parameters) == 2
 
-    instantiator = stormpy.pars.PDtmcInstantiator(model)
+    instantiator = stormpy.pars.ModelInstantiator[stormpy.ModelType.DTMC, float](model)
     point = dict()
     for x in parameters:
         print(x.name)

lib/stormpy/_template.py

@@ -0,0 +1,250 @@
+"""Runtime representation and metadata for native C++ template families.
+
+C++ template specializations still need to be compiled and bound separately.
+``TemplateClass`` groups those concrete Python classes behind one public,
+subscriptable object and exposes their structure to documentation and stub
+generation tools.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Callable, Iterator, Mapping, Sequence
+from dataclasses import dataclass
+from types import MappingProxyType
+from typing import Any, Literal, TypeAlias
+
+TemplateParameterKind: TypeAlias = Literal["type", "value"]
+
+
+@dataclass(frozen=True)
+class TemplateParameter:
+    """Description of one public template parameter.
+
+    ``type`` parameters select a Python or native type. ``value`` parameters
+    select a runtime value, such as a ``ModelType`` enum member.
+    """
+
+    name: str
+    kind: TemplateParameterKind = "type"
+
+
+@dataclass(frozen=True)
+class TemplateInstantiation:
+    """Description of one concrete native template specialization."""
+
+    arguments: tuple[object, ...]
+    implementation: type
+    native_name: str
+
+
+@dataclass(frozen=True)
+class TemplateMetadata:
+    """Tooling-oriented description of a complete template family."""
+
+    name: str
+    canonical_name: str
+    parameters: tuple[TemplateParameter, ...]
+    instantiations: tuple[TemplateInstantiation, ...]
+    deduction_guide: str | None
+
+
+DeductionGuide: TypeAlias = Callable[["TemplateClass", tuple[Any, ...], Mapping[str, Any]], object]
+
+
+def deduce_from_first_argument(source: "TemplateClass | None" = None, *, keyword: str | None = None) -> DeductionGuide:
+    """Create a guide that copies template arguments from an instance.
+
+    The first positional constructor argument is used when present. ``keyword``
+    optionally identifies the same argument for keyword-only calls. If
+    ``source`` is omitted, the instance is matched against the family being
+    constructed; otherwise it is matched against ``source``.
+    """
+
+    def deduction(family: TemplateClass, args: tuple[Any, ...], kwargs: Mapping[str, Any]) -> object:
+        if args:
+            instance = args[0]
+        elif keyword is not None and keyword in kwargs:
+            instance = kwargs[keyword]
+        else:
+            argument = f"{keyword!r}" if keyword is not None else " first positional"
+            raise TypeError(f"Cannot deduce template parameters without the {argument} argument")
+        return (source if source is not None else family).parameters_of(instance)
+
+    deduction.__name__ = "deduce_from_first_argument"
+    deduction.__qualname__ = "deduce_from_first_argument"
+    return deduction
+
+
+class TemplateClass:
+    """Native C++ template family exposed as a subscriptable Python object.
+
+    ``family[parameters]`` returns a registered concrete Python class.
+    ``family(*args, **kwargs)`` constructs a class selected by a configured
+    deduction guide.
+    """
+
+    def __init__(
+        self,
+        canonical_name: str,
+        module: object,
+        *,
+        parameters: Sequence[str | TemplateParameter],
+        deduce: DeductionGuide | None = None,
+    ) -> None:
+        """Load a native template family.
+
+        :param canonical_name: Fully qualified public family name used for
+            native registration lookup, tooling, and representations. Its last
+            component is the native template-family name.
+        :param module: Native module containing the registered specializations.
+        :param parameters: Ordered descriptions or names of the public
+            template parameters. A bare name describes a type parameter.
+        :param deduce: Optional constructor deduction guide. It receives this
+            family, the positional constructor arguments, and a read-only
+            mapping of keyword arguments, and returns the complete template
+            parameter tuple. Deduction guides may inspect any constructor
+            argument and may provide defaults or transform parameters.
+        :raises RuntimeError: If the module has no registrations for ``name``,
+            has an empty registration table, or mixes parameter arities.
+        :raises ValueError: If parameter metadata or the canonical name is
+            invalid.
+        """
+        canonical_module, separator, name = canonical_name.rpartition(".")
+        if not separator or not canonical_module or not name.isidentifier():
+            raise ValueError("Canonical template name must be fully qualified")
+
+        try:
+            implementations = module._template_instantiations[name]
+        except (AttributeError, KeyError):
+            raise RuntimeError(f"Native module has no registrations for {name}") from None
+        if not implementations:
+            raise RuntimeError(f"Native module has no registrations for {name}")
+
+        arities = {len(arguments) for arguments in implementations}
+        if len(arities) != 1:
+            raise RuntimeError(f"Native module has inconsistent registrations for {name}")
+
+        parameter_metadata = tuple(parameter if isinstance(parameter, TemplateParameter) else TemplateParameter(parameter) for parameter in parameters)
+        arity = arities.pop()
+        if len(parameter_metadata) != arity:
+            raise ValueError(f"{name} has {arity} native template parameters, but {len(parameter_metadata)} parameter names were provided")
+        if any(not parameter.name or not parameter.name.isidentifier() for parameter in parameter_metadata):
+            raise ValueError(f"Invalid template parameter name for {name}")
+        if any(parameter.kind not in ("type", "value") for parameter in parameter_metadata):
+            raise ValueError(f"Invalid template parameter kind for {name}")
+        if len({parameter.name for parameter in parameter_metadata}) != arity:
+            raise ValueError(f"Template parameter names for {name} must be unique")
+
+        self.__name__ = name
+        self.__qualname__ = name
+        self.__module__ = canonical_module
+        self._canonical_name = canonical_name
+        self._parameters = parameter_metadata
+        self._arity = arity
+        self._deduction_guide = deduce
+        self._instantiations: dict[tuple[object, ...], type] = {}
+        self._parameters_by_type: dict[type, tuple[object, ...]] = {}
+        for arguments, implementation in implementations.items():
+            self.register(arguments, implementation)
+
+    def _normalize(self, parameters: object) -> tuple[object, ...]:
+        """Convert subscription parameters to a validated tuple."""
+        key = parameters if isinstance(parameters, tuple) else (parameters,)
+        if len(key) != self._arity:
+            raise TypeError(f"{self.__name__} expects {self._arity} template parameter{'s' if self._arity != 1 else ''}, got {len(key)}")
+        return key
+
+    def register(self, parameters: object, implementation: type) -> None:
+        """Add a concrete specialization to this family.
+
+        :param parameters: One parameter or a tuple containing the complete
+            template-parameter list.
+        :param implementation: Concrete Python class for those parameters.
+        :raises TypeError: If the parameter count is wrong or ``implementation``
+            is not a class.
+        :raises ValueError: If the parameter tuple or implementation class is
+            already registered.
+        """
+        key = self._normalize(parameters)
+        if not isinstance(implementation, type):
+            raise TypeError("A template implementation must be a class")
+        if key in self._instantiations:
+            raise ValueError(f"{self.__name__} instantiation for {key!r} is already registered")
+        if implementation in self._parameters_by_type:
+            other_key = self._parameters_by_type[implementation]
+            raise ValueError(f"{self.__name__} implementation {implementation!r} is already registered for {other_key!r}")
+        self._instantiations[key] = implementation
+        self._parameters_by_type[implementation] = key
+
+    def __getitem__(self, parameters: object) -> type:
+        """Return the concrete class registered for ``parameters``.
+
+        A single parameter may be written directly as ``family[T]``; multiple
+        parameters use normal subscription tuple syntax, ``family[T, U]``.
+
+        :raises TypeError: If the parameter count is wrong or no matching
+            specialization is registered.
+        """
+        key = self._normalize(parameters)
+        try:
+            return self._instantiations[key]
+        except KeyError:
+            raise TypeError(f"{self.__name__} has no instantiation for {key!r}") from None
+
+    def __call__(self, *args: Any, **kwargs: Any) -> Any:
+        """Construct the specialization selected by the deduction guide.
+
+        :raises TypeError: If no deduction guide is configured or the deduced
+            specialization is unavailable.
+        """
+        if self._deduction_guide is None:
+            raise TypeError(f"{self.__name__} requires explicit template parameters")
+        parameters = self._deduction_guide(self, args, MappingProxyType(kwargs))
+        return self[parameters](*args, **kwargs)
+
+    def parameters_of(self, instance: object) -> tuple[object, ...]:
+        """Return the complete parameter tuple of a registered instance.
+
+        The runtime type must be an exact registered implementation; instances
+        of unregistered subclasses are not recognized.
+
+        :raises TypeError: If the instance's runtime type is not registered.
+        """
+        try:
+            return self._parameters_by_type[type(instance)]
+        except KeyError:
+            raise TypeError(f"Cannot infer {self.__name__} template parameters from {type(instance)!r}") from None
+
+    @property
+    def canonical_name(self) -> str:
+        """Fully qualified public name of this template family."""
+        return self._canonical_name
+
+    @property
+    def metadata(self) -> TemplateMetadata:
+        """Return an immutable, current description for documentation tools."""
+        instantiations = tuple(
+            TemplateInstantiation(parameters, implementation, f"{implementation.__module__}.{implementation.__name__}")
+            for parameters, implementation in self._instantiations.items()
+        )
+        guide = None
+        if self._deduction_guide is not None:
+            guide = getattr(self._deduction_guide, "__qualname__", type(self._deduction_guide).__qualname__)
+        return TemplateMetadata(self.__name__, self._canonical_name, self._parameters, instantiations, guide)
+
+    @property
+    def instantiations(self) -> Mapping[tuple[object, ...], type]:
+        """Map registered parameter tuples to classes without allowing mutation."""
+        return MappingProxyType(self._instantiations)
+
+    def is_instantiation(self, instance: object) -> bool:
+        """Return whether ``instance`` has a registered concrete runtime type."""
+        return type(instance) in self._parameters_by_type
+
+    def __iter__(self) -> Iterator[tuple[object, ...]]:
+        """Iterate over registered parameter tuples in registration order."""
+        return iter(self._instantiations)
+
+    def __repr__(self) -> str:
+        """Return a concise template-family representation."""
+        return f"<template class {self._canonical_name}>"

lib/stormpy/dft/__init__.py

@@ -6,58 +6,71 @@
 from . import _dft
 from ._dft import *
 from .modules import modules_json
+from stormpy._template import TemplateClass, deduce_from_first_argument as _deduce_from_first_argument
 
 _dft._set_up()
 
 
-def analyze_dft(ft, properties, symred=True, allow_modularisation=False, relevant_events=RelevantEvents(), allow_dc_for_relevant=False):
-    if isinstance(ft, DFT_double):
-        return _dft._analyze_dft_double(ft, properties, symred, allow_modularisation, relevant_events, allow_dc_for_relevant)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._analyze_dft_ratfunc(ft, properties, symred, allow_modularisation, relevant_events, allow_dc_for_relevant)
+DFT = TemplateClass(
+    "stormpy.dft.DFT",
+    _dft,
+    parameters=("ValueType",),
+    deduce=_deduce_from_first_argument(keyword="dft"),
+)
 
+DFTElement = TemplateClass(
+    "stormpy.dft.DFTElement",
+    _dft,
+    parameters=("ValueType",),
+)
 
-def build_model(ft, symmetries=DftSymmetries(), relevant_events=RelevantEvents(), allow_dc_for_relevant=False):
-    if isinstance(ft, DFT_double):
-        return _dft._build_model_double(ft, symmetries, relevant_events, allow_dc_for_relevant)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._build_model_ratfunc(ft, symmetries, relevant_events, allow_dc_for_relevant)
+DFTBE = TemplateClass(
+    "stormpy.dft.DFTBE",
+    _dft,
+    parameters=("ValueType",),
+)
 
+DFTDependency = TemplateClass(
+    "stormpy.dft.DFTDependency",
+    _dft,
+    parameters=("ValueType",),
+)
 
-def transform_dft(ft, unique_constant_be, binary_fdeps, exponential_distributions):
-    if isinstance(ft, DFT_double):
-        return _dft._transform_dft_double(ft, unique_constant_be, binary_fdeps, exponential_distributions)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._transform_dft_ratfunc(ft, unique_constant_be, binary_fdeps, exponential_distributions)
+DFTState = TemplateClass(
+    "stormpy.dft.DFTState",
+    _dft,
+    parameters=("ValueType",),
+)
 
+DFTSimulator = TemplateClass(
+    "stormpy.dft.DFTSimulator",
+    _dft,
+    parameters=("ValueType",),
+    deduce=_deduce_from_first_argument(DFT, keyword="dft"),
+)
 
-def compute_dependency_conflicts(ft, use_smt=False, solver_timeout=0):
-    if isinstance(ft, DFT_double):
-        return _dft._compute_dependency_conflicts_double(ft, use_smt, solver_timeout)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._compute_dependency_conflicts_ratfunc(ft, use_smt, solver_timeout)
+ExplicitDFTModelBuilder = TemplateClass(
+    "stormpy.dft.ExplicitDFTModelBuilder",
+    _dft,
+    parameters=("ValueType",),
+    deduce=_deduce_from_first_argument(DFT, keyword="dft"),
+)
 
+_deduce_dft_parameters = _deduce_from_first_argument(DFT, keyword="dft")
 
-def prepare_for_analysis(ft):
-    compute_dependency_conflicts(ft, use_smt=False)
-    return transform_dft(ft, unique_constant_be=True, binary_fdeps=True, exponential_distributions=True)
+
+def _deduce_dft_instantiator(family, args, kwargs):
+    return (*_deduce_dft_parameters(family, args, kwargs), float)
 
 
-def is_well_formed(ft, check_valid_for_analysis=True):
-    if isinstance(ft, DFT_double):
-        return _dft._is_well_formed_double(ft, check_valid_for_analysis)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._is_well_formed_ratfunc(ft, check_valid_for_analysis)
+DFTInstantiator = TemplateClass(
+    "stormpy.dft.DFTInstantiator",
+    _dft,
+    parameters=("SourceValueType", "TargetValueType"),
+    deduce=_deduce_dft_instantiator,
+)
 
 
-def has_potential_modeling_issues(ft):
-    if isinstance(ft, DFT_double):
-        return _dft._has_potential_modeling_issues_double(ft)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._has_potential_modeling_issues_ratfunc(ft)
+def prepare_for_analysis(ft):
+    compute_dependency_conflicts(ft, use_smt=False)
+    return transform_dft(ft, unique_constant_be=True, binary_fdeps=True, exponential_distributions=True)