Source code for momba.model.types
# -*- coding:utf-8 -*-
#
# Copyright (C) 2019-2021, Saarland University
# Copyright (C) 2019-2021, Maximilian Köhl <koehl@cs.uni-saarland.de>
from __future__ import annotations
import dataclasses as d
import typing as t
import abc
from . import errors, expressions
if t.TYPE_CHECKING:
from . import context
class BaseTypeError(errors.TypeConstructionError):
pass
class InvalidBoundError(errors.TypeConstructionError):
pass
Bound = t.Optional[t.Union["expressions.ValueOrExpression", "ellipsis"]] # noqa: F821
[docs]
class Type(abc.ABC):
"""
A *type*.
"""
@property
def is_numeric(self) -> bool:
"""
Indicates whether the type is numeric or not.
"""
return False
[docs]
@abc.abstractmethod
def is_assignable_from(self, typ: Type) -> bool:
"""
Checks whether values of the other type can be assigned to
targets of this type.
"""
raise NotImplementedError()
def validate_in(self, scope: context.Scope) -> None: # noqa: B027
pass
[docs]
class NumericType(Type, abc.ABC):
@property
def is_numeric(self) -> bool:
return True
[docs]
def bound(self, lower: Bound, upper: Bound) -> BoundedType:
"""
Bounds the numeric type with the given bounds.
"""
return BoundedType(
self, BoundedType.convert_bound(lower), BoundedType.convert_bound(upper)
)
[docs]
@d.dataclass(frozen=True)
class IntegerType(NumericType):
"""
The *integer type*.
.. hint::
Instead of instantiating new objects of this class use :attr:`INT`.
"""
def __str__(self) -> str:
return "types.INT"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
if isinstance(typ, BoundedType):
return typ.base == INT
return typ == INT
[docs]
@d.dataclass(frozen=True)
class RealType(NumericType):
"""
The *real type*.
.. hint::
Instead of instantiating new objects of this class use :attr:`REAL`.
"""
def __str__(self) -> str:
return "types.REAL"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
return typ.is_numeric
[docs]
@d.dataclass(frozen=True)
class BoolType(Type):
"""
The *boolean type*.
.. hint::
Instead of instantiating new objects of this class use :attr:`BOOL`.
"""
def __str__(self) -> str:
return "types.BOOL"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
return typ == BOOL
[docs]
@d.dataclass(frozen=True)
class ClockType(NumericType):
"""
The *clock type*.
.. hint::
Instead of instantiating new objects of this class use :attr:`CLOCK`.
"""
def __str__(self) -> str:
return "types.CLOCK"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
if isinstance(typ, BoundedType):
return typ.base == INT
return typ == INT
[docs]
@d.dataclass(frozen=True)
class ContinuousType(NumericType):
"""
The *continuous type*.
.. hint::
Instead of instantiating new objects of this class use :attr:`CONTINUOUS`.
"""
def __str__(self) -> str:
return "types.CONTINUOUS"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
return typ.is_numeric
INT = IntegerType()
REAL = RealType()
BOOL = BoolType()
CLOCK = ClockType()
CONTINUOUS = ContinuousType()
[docs]
@d.dataclass(frozen=True)
class BoundedType(NumericType):
"""
A *bounded numeric type*.
Attributes
----------
base:
The numeric base type.
lower_bound:
The optional lower bound for values of the type.
upper_bound:
The optional upper bound for values of the type.
"""
base: NumericType
lower_bound: t.Optional[expressions.Expression]
upper_bound: t.Optional[expressions.Expression]
def __str__(self) -> str:
return f"{self.base}[{self.lower_bound}, {self.upper_bound}]"
def __post_init__(self) -> None:
if not isinstance(self.base, NumericType):
raise BaseTypeError("base-type of bounded type must be numeric")
if self.lower_bound is None and self.upper_bound is None:
raise InvalidBoundError(
"neither `lower_bound` nor `upper_bound` is present"
)
def validate_in(self, scope: context.Scope) -> None:
if self.lower_bound is not None:
# if not scope.is_constant(self.lower_bound):
# raise InvalidBoundError("`lower_bound` has to be a constant")
lower_bound_type = scope.get_type(self.lower_bound)
if not self.base.is_assignable_from(lower_bound_type):
raise InvalidBoundError(
f"type {lower_bound_type} of `lower_bound` is not "
f"assignable to base-type {self.base}"
)
if self.upper_bound is not None:
# if not scope.is_constant(self.upper_bound):
# raise InvalidBoundError("`upper_bound` has to be a constant")
upper_bound_type = scope.get_type(self.upper_bound)
if not self.base.is_assignable_from(upper_bound_type):
raise InvalidBoundError(
f"type {upper_bound_type} of `upper_bound` is not "
f"assignable to base-type {self.base}"
)
@staticmethod
def convert_bound(bound: Bound) -> t.Optional[expressions.Expression]:
if bound is None or bound is Ellipsis:
return None
return expressions.ensure_expr(t.cast(expressions.ValueOrExpression, bound))
[docs]
def is_assignable_from(self, typ: Type) -> bool:
return self.base.is_assignable_from(typ)
[docs]
@d.dataclass(frozen=True)
class ArrayType(Type):
"""
An *array type*.
Attributes
----------
element:
The type of the elements of the array.
"""
element: Type
def __str__(self) -> str:
return f"Array({self.element})"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
return isinstance(typ, ArrayType) and self.element.is_assignable_from(
typ.element
)
[docs]
def array_of(element: Type) -> ArrayType:
"""
Constructs an array type with the given element type.
"""
return ArrayType(element)
[docs]
@d.dataclass(frozen=True)
class SetType(Type):
"""
An *set type*.
Attributes
----------
element:
The type of the elements of the set.
"""
element: Type
def __str__(self) -> str:
return f"Set({self.element})"
[docs]
def is_assignable_from(self, typ: Type) -> bool:
return isinstance(typ, SetType) and self.element.is_assignable_from(typ.element)
[docs]
def set_of(element: Type) -> SetType:
"""
Constructs a set type with the given element type.
"""
return SetType(element)
@d.dataclass(frozen=True)
class StateType(Type):
def __str__(self) -> str:
return "types.STATE"
def is_assignable_from(self, typ: Type) -> bool:
return typ == STATE
STATE = StateType()
class InferTypeUnary(t.Protocol):
def __call__(self, operand: Type) -> Type:
pass
class InferTypeBinary(t.Protocol):
def __call__(self, left: Type, right: Type) -> Type:
pass
