Dimensions (guardrail_calculus.dimensions)

Concrete temporal values and the symbolic conditional, built on the kernel's dimensional protocols.

dimensions

Concrete temporal/dimensional values and the symbolic conditional.

Time and duration dimensionality is separated from the rest of the public DSL surface. This module builds on the import-safe guardrail_kernel package; it does not import the public guardrail_calculus package itself.

NodeT module-attribute

NodeT = TypeVar('NodeT')

UTime module-attribute

UTime = TypeVar('UTime', bound=TimeLike)

TDuration module-attribute

TDuration = TypeVar('TDuration', bound=DurationLike)

MinutesBound module-attribute

MinutesBound = int | TypeForm[int]

MinutesT module-attribute

MinutesT = TypeVar('MinutesT', bound=MinutesBound)

CondT module-attribute

CondT = TypeVar('CondT', bound=BoolLike)

ThenT module-attribute

ThenT = TypeVar('ThenT')

ElseT module-attribute

ElseT = TypeVar('ElseT')

t module-attribute

t = ClockLiteralFactory()

Duration dataclass

Bases: _SymbolicEquality, DimensionIdentity[Literal['Duration']]

A span of minutes (the duration dimension).

Arithmetic operations on Duration produce DurationExpr or TimeExpr.

Attributes:

Name	Type	Description
minutes	int	The raw integer minute span.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, order=True)
class Duration(_SymbolicEquality, DimensionIdentity[Literal["Duration"]]):
    """A span of minutes (the *duration* dimension).

    Arithmetic operations on [Duration][guardrail_calculus.dimensions.Duration] produce
    [DurationExpr][guardrail_calculus.dimensions.DurationExpr] or
    [TimeExpr][guardrail_calculus.dimensions.TimeExpr].

    Attributes:
        minutes: The raw integer minute span.
    """

    minutes: int
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = DURATION

    minutes_: typing.ClassVar = DURATION_CONSTRUCTORS.minutes_
    hours: typing.ClassVar = DURATION_CONSTRUCTORS.hours
    hm: typing.ClassVar = DURATION_CONSTRUCTORS.hm

    @property
    def label(self) -> str:
        return f"{self.minutes} minutes"

    @overload
    def __add__(self, other: TDuration) -> DurationExpr[_Add[Duration, TDuration]]: ...

    @overload
    def __add__(self, other: UTime) -> TimeExpr[_Add[Duration, UTime]]: ...

    def __add__(self, other: Any) -> Any:
        return _apply("+", self, other)

    def __sub__(
        self, other: TDuration
    ) -> DurationExpr[_Sub[Duration, TDuration]]:
        return _apply("-", self, other)

    def __mul__(self, other: Any) -> Any:
        return _apply("*", self, other)

    def __rmul__(self, other: Any) -> Any:
        return _apply("*", other, self)

minutes instance-attribute

minutes

minutes_ class-attribute instance-attribute

minutes_ = minutes_

hours class-attribute instance-attribute

hours = hours

hm class-attribute instance-attribute

hm = hm

label property

label

ClockTimeHmConstructor

Bases: Protocol

Source code in src/guardrail_calculus/dimensions.py

class ClockTimeHmConstructor(typing.Protocol):
    def __call__(self, hour: int, minute: int = 0) -> ClockTime[int]: ...

ClockTime dataclass

Bases: _SymbolicEquality, DimensionIdentity[Literal['Instant']], Generic[MinutesT]

A concrete clock instant, stored as minutes-of-day (the time dimension).

The minute count is kept in the type parameter (ClockTime[Literal[545]]) so a literal departure time survives into the static witness.

Attributes:

Name	Type	Description
minutes	MinutesT	The minutes of day.

Source code in src/guardrail_calculus/dimensions.py

@dataclass(frozen=True, order=True)
class ClockTime(_SymbolicEquality, DimensionIdentity[Literal["Instant"]], Generic[MinutesT]):
    """A concrete clock instant, stored as minutes-of-day (the *time* dimension).

    The minute count is kept in the type parameter (`ClockTime[Literal[545]]`)
    so a literal departure time survives into the static witness.

    Attributes:
        minutes: The minutes of day.
    """

    minutes: MinutesT
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = INSTANT

    def minutes_as_int(self) -> int:
        assert isinstance(self.minutes, int), "minutes must be an int"
        return self.minutes

    hm: typing.ClassVar[ClockTimeHmConstructor] = INSTANT_CONSTRUCTORS.hm  # type: ignore[assignment]

    @property
    def label(self) -> str:
        return str(self)

    def __add__(
        self: typing_extensions.Self,
        other: TDuration,
    ) -> TimeExpr[_Add[typing_extensions.Self, TDuration]]:
        return _apply("+", self, other)

    @overload
    def __sub__(
        self: typing_extensions.Self,
        other: TDuration,
    ) -> TimeExpr[_Sub[typing_extensions.Self, TDuration]]: ...

    @overload
    def __sub__(
        self: typing_extensions.Self,
        other: UTime,
    ) -> DurationExpr[_Sub[typing_extensions.Self, UTime]]: ...

    def __sub__(self: typing_extensions.Self, other: object) -> Any:
        return _apply("-", self, other)

    def __str__(self) -> str:
        hour, minute = divmod(self.minutes_as_int(), 60)
        return f"{hour:02d}:{minute:02d}"

    _from_hhmm: typing.ClassVar = INSTANT_CONSTRUCTORS.from_hhmm
    @classmethod
    def from_hhmm[T: int](cls, param: typing_extensions.TypeForm[T] | T | ClockTime[T] | ClockTime[typing_extensions.TypeForm[T]]) -> ClockTime[T]:
        if isinstance(param, cls):  # pragma: no cover
            if not isinstance(param.minutes, int):
                return cast(ClockTime[T], cls.from_hhmm(param.minutes))
            return cast(ClockTime[T], param)
        if inspect.isclass(param) and issubclass(param, cls):  # pragma: no cover
            return cls.from_hhmm(typing_extensions.get_args(param)[0])
        if isinstance(param, int):
            assert isinstance(param, int), "param must be an int"
            raw_int = param
        elif typing_extensions.get_origin(param) is typing_extensions.Literal:
            raw_int = typing_extensions.get_args(param)[0]
        elif typing_extensions.get_origin(param) is cls:
            return cls.from_hhmm(typing_extensions.get_args(param)[0])
        else:
            raise TypeError(f"Cannot create ClockTime from {param}")
        return typing.cast(
            ClockTime[T], cls._from_hhmm(raw_int))

minutes instance-attribute

minutes

hm class-attribute

hm = hm

label property

label

minutes_as_int

minutes_as_int()

Source code in src/guardrail_calculus/dimensions.py

def minutes_as_int(self) -> int:
    assert isinstance(self.minutes, int), "minutes must be an int"
    return self.minutes

from_hhmm classmethod

from_hhmm(param)

Source code in src/guardrail_calculus/dimensions.py

@classmethod
def from_hhmm[T: int](cls, param: typing_extensions.TypeForm[T] | T | ClockTime[T] | ClockTime[typing_extensions.TypeForm[T]]) -> ClockTime[T]:
    if isinstance(param, cls):  # pragma: no cover
        if not isinstance(param.minutes, int):
            return cast(ClockTime[T], cls.from_hhmm(param.minutes))
        return cast(ClockTime[T], param)
    if inspect.isclass(param) and issubclass(param, cls):  # pragma: no cover
        return cls.from_hhmm(typing_extensions.get_args(param)[0])
    if isinstance(param, int):
        assert isinstance(param, int), "param must be an int"
        raw_int = param
    elif typing_extensions.get_origin(param) is typing_extensions.Literal:
        raw_int = typing_extensions.get_args(param)[0]
    elif typing_extensions.get_origin(param) is cls:
        return cls.from_hhmm(typing_extensions.get_args(param)[0])
    else:
        raise TypeError(f"Cannot create ClockTime from {param}")
    return typing.cast(
        ClockTime[T], cls._from_hhmm(raw_int))

ClockLiteralFactory

A factory class allowing t[1730] syntax to build literal ClockTimes.

Source code in src/guardrail_calculus/dimensions.py

class ClockLiteralFactory:
    """A factory class allowing `t[1730]` syntax to build literal [ClockTime][guardrail_calculus.dimensions.ClockTime]s."""
    @overload
    def __getitem__[HHMMT: int](self, value: typing_extensions.TypeForm[HHMMT]) -> ClockTime[HHMMT]: ...

    @overload
    def __getitem__[HHMMT: int](self, value: HHMMT) -> ClockTime[HHMMT]: ...

    def __getitem__[HHMMT: int](self, value: HHMMT | typing_extensions.TypeForm[HHMMT]) -> ClockTime[HHMMT]:
        return cast(ClockTime[HHMMT], ClockTime.from_hhmm(value))

TimePoint dataclass

Bases: DimensionIdentity[Literal['Instant']], TimeComparableMixin

A symbolic time instant referenced by path, e.g. drew.departure.

Attributes:

Name	Type	Description
path	Path	The path descriptor to the symbolic time instant.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=False)
class TimePoint(DimensionIdentity[Literal["Instant"]], TimeComparableMixin):
    """A symbolic time instant referenced by path, e.g. `drew.departure`.

    Attributes:
        path: The path descriptor to the symbolic time instant.
    """

    path: Path
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = INSTANT

    @property
    def label(self) -> str:
        return self.path.display

    def __matmul__(self, other: UTime) -> BoolExpr[_Eq[TimePoint, UTime]]:
        if _coerce_dimension_operand(self, other) is _REJECTED:
            return NotImplemented
        return eq_pred(self, other)

    def __add__(self, other: TDuration) -> TimeExpr[_Add[TimePoint, TDuration]]:
        return add_duration_to_time_or_not_implemented(self, other, _Add)

    @overload
    def __sub__(self, other: TDuration) -> TimeExpr[_Sub[TimePoint, TDuration]]: ...

    @overload
    def __sub__(self, other: UTime) -> DurationExpr[_Sub[TimePoint, UTime]]: ...

    def __sub__(self, other: object) -> Any:
        return _time_sub(self, other)

    def __str__(self) -> str:
        return self.label

path instance-attribute

path

label property

label

BoundTimePoint dataclass

Bases: DimensionIdentity[Literal['Instant']], TimeComparableMixin

Time observable of the current subject block.

Runtime binding rewrites _.departure inside field blake=subject(...) into blake.departure.

Example

blake = subject().given(_.departure == drew.departure - Duration.hours(1))

Attributes:

Name	Type	Description
observable	str	The name of the field on the current subject.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=False)
class BoundTimePoint(DimensionIdentity[Literal["Instant"]], TimeComparableMixin):
    """Time observable of the current subject block.

    Runtime binding rewrites `_.departure` inside field `blake=subject(...)` into `blake.departure`.

    Example:
        ```python
        blake = subject().given(_.departure == drew.departure - Duration.hours(1))
        ```

    Attributes:
        observable: The name of the field on the current subject.
    """

    observable: str
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = INSTANT

    @property
    def label(self) -> str:
        return f"_.{self.observable}"

    def bind(self, subject_name: str) -> TimePoint:
        return TimePoint(Path((subject_name, self.observable)))

    def __matmul__(self, other: UTime) -> BoolExpr[_Eq[BoundTimePoint, UTime]]:
        if _coerce_dimension_operand(self, other) is _REJECTED:
            return NotImplemented
        return eq_pred(self, other)

    def __add__(self, other: TDuration) -> TimeExpr[_Add[BoundTimePoint, TDuration]]:
        return add_duration_to_time_or_not_implemented(self, other, _Add)

    @overload
    def __sub__(
        self, other: TDuration
    ) -> TimeExpr[_Sub[BoundTimePoint, TDuration]]: ...

    @overload
    def __sub__(self, other: UTime) -> DurationExpr[_Sub[BoundTimePoint, UTime]]: ...

    def __sub__(self, other: object) -> Any:
        return _time_sub(self, other)

observable instance-attribute

observable

label property

label

bind

bind(subject_name)

Source code in src/guardrail_calculus/dimensions.py

def bind(self, subject_name: str) -> TimePoint:
    return TimePoint(Path((subject_name, self.observable)))

SubjectRefProtocol

Bases: Protocol

Protocol for classes that act as references to a subject with a departure time.

Source code in src/guardrail_calculus/dimensions.py

class SubjectRefProtocol[TP: TimeLike](typing.Protocol):
    """Protocol for classes that act as references to a subject with a departure time."""

    @property
    def departure(self) -> TP: ...

departure property

departure

SubjectRef dataclass

A reference to another subject in the puzzle.

Attributes:

Name	Type	Description
path	Path	The path to the referenced subject.

Source code in src/guardrail_calculus/dimensions.py

@dataclass(frozen=True)
class SubjectRef:
    """A reference to another subject in the puzzle.

    Attributes:
        path: The path to the referenced subject.
    """
    path: Path

    @property
    def departure(self) -> TimePoint:
        return TimePoint(self.path.child("departure"))

path instance-attribute

path

departure property

departure

DurationExpr dataclass

Bases: _ExprNode[NodeT], _ScalarMul, DimensionIdentity[Literal['Duration']], DurationComparableMixin

A composite duration expression (e.g. the result of time - time).

Attributes:

Name	Type	Description
node	NodeT	The underlying provenance node.
label	str	The expression label.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=False)
class DurationExpr(
    _ExprNode[NodeT],
    _ScalarMul,
    DimensionIdentity[Literal["Duration"]],
    DurationComparableMixin,
):
    """A composite duration expression (e.g. the result of `time - time`).

    Attributes:
        node: The underlying provenance node.
        label: The expression label.
    """

    node: NodeT
    label: str
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = DURATION

    def __add__(
        self, other: TDuration
    ) -> DurationExpr[_Add[DurationExpr[NodeT], TDuration]]:
        return _apply("+", self, other)

    def __sub__(
        self, other: TDuration
    ) -> DurationExpr[_Sub[DurationExpr[NodeT], TDuration]]:
        return _apply("-", self, other)

node instance-attribute

node

label instance-attribute

label

TimeExpr dataclass

Bases: _ExprNode[NodeT], DimensionIdentity[Literal['Instant']], TimeComparableMixin

A composite time expression (e.g. the result of time + duration).

Attributes:

Name	Type	Description
node	NodeT	The underlying provenance node.
label	str	The expression label.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=False)
class TimeExpr(
    _ExprNode[NodeT],
    DimensionIdentity[Literal["Instant"]],
    TimeComparableMixin,
):
    """A composite time expression (e.g. the result of `time + duration`).

    Attributes:
        node: The underlying provenance node.
        label: The expression label.
    """

    node: NodeT
    label: str
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = INSTANT

    def __add__(self, other: TDuration) -> TimeExpr[_Add[TimeExpr[NodeT], TDuration]]:
        return _apply("+", self, other)

    @overload
    def __sub__(
        self, other: TDuration
    ) -> TimeExpr[_Sub[TimeExpr[NodeT], TDuration]]: ...

    @overload
    def __sub__(self, other: UTime) -> DurationExpr[_Sub[TimeExpr[NodeT], UTime]]: ...

    def __sub__(self, other: object) -> Any:
        return _apply("-", self, other)

    def __str__(self) -> str:
        return self.label

node instance-attribute

node

label instance-attribute

label

DimensionExpr dataclass

Bases: _ExprNode[NodeT], _ScalarMul, DimensionIdentity[Any], _ComparableRuntime

A generic composite dimension expression (e.g. for user-defined dimensions).

Attributes:

Name	Type	Description
node	NodeT	The underlying provenance node.
label	str	The expression label.
unit	str | None	Optional unit string.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=False)
class DimensionExpr(
    _ExprNode[NodeT],
    _ScalarMul,
    DimensionIdentity[Any],
    _ComparableRuntime,
):
    """A generic composite dimension expression (e.g. for user-defined dimensions).

    Attributes:
        node: The underlying provenance node.
        label: The expression label.
        unit: Optional unit string.
    """

    node: NodeT
    label: str
    _dimension: Dimension[Any] = field(kw_only=True)
    unit: str | None = None

    def __add__(self, other: Any) -> Any:
        return _apply("+", self, other)

    def __sub__(self, other: Any) -> Any:
        return _apply("-", self, other)

node instance-attribute

node

label instance-attribute

label

unit class-attribute instance-attribute

unit = None

IfTime dataclass

Bases: _IfNode[CondT, ThenT, ElseT], DimensionIdentity[Literal['Instant']]

Symbolic if/then/else conditional returning an instant.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=True)
class IfTime[
    CondT: BoolLike,
    ThenT: TimeLike,
    ElseT: TimeLike,
](
    _IfNode[CondT, ThenT, ElseT],
    DimensionIdentity[Literal["Instant"]],
):
    """Symbolic if/then/else conditional returning an instant."""
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = INSTANT

IfDuration dataclass

Bases: _IfNode[CondT, ThenT, ElseT], DimensionIdentity[Literal['Duration']]

Symbolic if/then/else conditional returning a duration.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=True)
class IfDuration[
    CondT: BoolLike,
    ThenT: DurationLike,
    ElseT: DurationLike,
](
    _IfNode[CondT, ThenT, ElseT],
    DimensionIdentity[Literal["Duration"]],
):
    """Symbolic if/then/else conditional returning a duration."""
    _dimension: typing.ClassVar[
        Dimension[Carrier[int]]
    ] = DURATION

IfBool dataclass

Bases: _IfNode[CondT, ThenT, ElseT]

Symbolic if/then/else conditional returning a boolean.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=True)
class IfBool[
    CondT: BoolLike,
    ThenT: BoolLike,
    ElseT: BoolLike,
](_IfNode[CondT, ThenT, ElseT]):
    """Symbolic if/then/else conditional returning a boolean."""
    _z3_dim: Literal["bool"] = field(
        default="bool",
        init=False,
        repr=False,
        compare=False,
    )

IfDimensionExpr dataclass

Bases: _IfNode[CondT, ThenT, ElseT], DimensionIdentity[Any]

Symbolic if/then/else conditional returning a generic dimension expression.

Source code in src/guardrail_calculus/dimensions.py

@typing.final
@dataclass(frozen=True, eq=True)
class IfDimensionExpr[
    CondT: BoolLike,
    ThenT: DimensionLike[Any],
    ElseT: DimensionLike[Any],
](
    _IfNode[CondT, ThenT, ElseT],
    DimensionIdentity[Any],
):
    """Symbolic if/then/else conditional returning a generic dimension expression."""
    _dimension: Dimension[Any] = field(kw_only=True)

time_at

time_at(hour, minute=0)

Helper to construct a ClockTime instance at HH:MM.

Parameters:

Name	Type	Description	Default
hour	int	The hour (0-23).	required
minute	int	The minute (0-59).	0

Returns:

Type	Description
ClockTime[int]	The constructed ClockTime instance.

Source code in src/guardrail_calculus/dimensions.py

def time_at(hour: int, minute: int = 0) -> ClockTime[int]:
    """Helper to construct a [ClockTime][guardrail_calculus.dimensions.ClockTime] instance at HH:MM.

    Args:
        hour: The hour (0-23).
        minute: The minute (0-59).

    Returns:
        The constructed ClockTime instance.
    """
    return ClockTime.hm(hour, minute)

fmt_time

fmt_time(minutes)

Format minutes of day into HH:MM.

Parameters:

Name	Type	Description	Default
minutes	int	The minutes.	required

Returns:

Type	Description
str	The formatted string.

Source code in src/guardrail_calculus/dimensions.py

def fmt_time(minutes: int) -> str:
    """Format minutes of day into HH:MM.

    Args:
        minutes: The minutes.

    Returns:
        The formatted string.
    """
    hour, minute = divmod(minutes, 60)
    return f"{hour:02d}:{minute:02d}"

add_duration_to_time_or_not_implemented

add_duration_to_time_or_not_implemented(
    left, right, node_factory
)

Internal helper to dispatch time + duration operations, or return NotImplemented.

Source code in src/guardrail_calculus/dimensions.py

def add_duration_to_time_or_not_implemented[
    LeftT: TimeLike,
    RightT: DurationLike,
    NodeT: ArithBinaryNode[Any, Any],
](
    left: LeftT,
    right: object,
    node_factory: type[NodeT],
) -> TimeExpr[NodeT] | types.NotImplementedType:
    """Internal helper to dispatch time + duration operations, or return NotImplemented."""
    return _apply(node_factory.label(), left, right)

duration_binary_or_not_implemented

duration_binary_or_not_implemented(
    left, right, node_factory
)

Internal helper to dispatch duration operations, or return NotImplemented.

Source code in src/guardrail_calculus/dimensions.py

def duration_binary_or_not_implemented[
    LeftT: DurationLike,
    NodeT: ArithBinaryNode[Any, Any],
](
    left: LeftT,
    right: object,
    node_factory: type[NodeT],
) -> DurationExpr[NodeT] | types.NotImplementedType:
    """Internal helper to dispatch duration operations, or return NotImplemented."""
    return _apply(node_factory.label(), left, right)

z3_if

z3_if(
    condition: CondT, then_: ThenT, else_: ElseT
) -> IfTime[CondT, ThenT, ElseT]

z3_if(
    condition: CondT, then_: ThenT, else_: ElseT
) -> IfDuration[CondT, ThenT, ElseT]

z3_if(
    condition: CondT, then_: ThenT, else_: ElseT
) -> IfBool[CondT, ThenT, ElseT]

z3_if(
    condition: CondT, then_: ThenT, else_: ElseT
) -> IfDimensionExpr[CondT, ThenT, ElseT]

z3_if(condition, then_, else_)

Symbolic if/then/else.

Returns then_ when condition is true, else_ otherwise. Chooses among IfTime, IfDuration, IfBool, and IfDimensionExpr by inspecting the types of then_ and else_.

Parameters:

Name	Type	Description	Default
condition	BoolLike	The symbolic boolean condition.	required
then_	object	The branch returned if the condition evaluates to true.	required
else_	object	The branch returned if the condition evaluates to false.	required

Returns:

Type	Description
Any	A symbolic branch wrapper.

Source code in src/guardrail_calculus/dimensions.py

def z3_if(
    condition: BoolLike,
    then_: object,
    else_: object,
) -> Any:
    """Symbolic if/then/else.

    Returns `then_` when condition is true, `else_` otherwise. Chooses among
    [IfTime][guardrail_calculus.dimensions.IfTime], [IfDuration][guardrail_calculus.dimensions.IfDuration],
    [IfBool][guardrail_calculus.dimensions.IfBool], and [IfDimensionExpr][guardrail_calculus.dimensions.IfDimensionExpr]
    by inspecting the types of `then_` and `else_`.

    Args:
        condition: The symbolic boolean condition.
        then_: The branch returned if the condition evaluates to true.
        else_: The branch returned if the condition evaluates to false.

    Returns:
        A symbolic branch wrapper.
    """
    if not is_bool_like(condition):
        raise TypeError(f"z3_if condition must be BoolLike, got {condition!r}")

    then_node = cast(Any, then_)
    else_node = cast(Any, else_)
    then_dim = dimension_of(then_)
    else_dim = dimension_of(else_)

    if then_dim is not None and else_dim is not None:
        if then_dim.name != else_dim.name:
            raise TypeError("z3_if branches must have the same expression dimension.")

        wrapper = _COND_WRAPPERS.get(then_dim.name)
        if wrapper is None:
            return IfDimensionExpr(
                condition=condition,
                then_=then_node,
                else_=else_node,
                label=(
                    f"if {condition.label} then {then_node.label} "
                    f"else {else_node.label}"
                ),
                _dimension=then_dim,
            )
    elif is_bool_like(then_) and is_bool_like(else_):
        wrapper = IfBool
    else:
        raise TypeError("z3_if branches must have the same expression dimension.")

    return wrapper(
        condition=condition,
        then_=then_node,
        else_=else_node,
        label=f"if {condition.label} then {then_node.label} else {else_node.label}",
    )

bind_value

bind_value(value, *, subject_name)

Recursively bind subject-bound placeholders (_.name) in a value.

Parameters:

Name	Type	Description	Default
value	object	The value to bind.	required
subject_name	str	The name of the subject to bind to.	required

Returns:

Type	Description
object	The bound object/expression.

Source code in src/guardrail_calculus/dimensions.py

def bind_value(value: object, *, subject_name: str) -> object:
    """Recursively bind subject-bound placeholders (`_.name`) in a value.

    Args:
        value: The value to bind.
        subject_name: The name of the subject to bind to.

    Returns:
        The bound object/expression.
    """
    if isinstance(value, BoundTimePoint):
        return value.bind(subject_name)

    if isinstance(value, BoolExpr):
        return bind_bool_expr(value, subject_name=subject_name)

    if isinstance(value, TimeExpr):
        return bind_time_expr(value, subject_name=subject_name)

    if isinstance(value, DurationExpr):
        return bind_duration_expr(value, subject_name=subject_name)

    if isinstance(value, (_Add, _Sub, _Eq, _Lt, _Le, _Gt, _Ge, _And, _Or)):
        return type(value)(
            bind_value(value.left, subject_name=subject_name),
            bind_value(value.right, subject_name=subject_name),
        )

    if isinstance(value, _Not):
        return _Not(bind_value(value.value, subject_name=subject_name))

    return value

bind_bool_expr

bind_bool_expr(expr, *, subject_name)

Bind subject-bound placeholders in a boolean expression.

Parameters:

Name	Type	Description	Default
expr	BoolExpr[NodeT]	The boolean expression.	required
subject_name	str	The subject name to bind to.	required

Returns:

Type	Description
BoolExpr[Any]	The bound expression.

Source code in src/guardrail_calculus/dimensions.py

def bind_bool_expr(expr: BoolExpr[NodeT], *, subject_name: str) -> BoolExpr[Any]:
    """Bind subject-bound placeholders in a boolean expression.

    Args:
        expr: The boolean expression.
        subject_name: The subject name to bind to.

    Returns:
        The bound expression.
    """
    return _rebind_expr(expr, BoolExpr, subject_name=subject_name)

bind_time_expr

bind_time_expr(expr, *, subject_name)

Bind subject-bound placeholders in a time expression.

Parameters:

Name	Type	Description	Default
expr	TimeExpr[NodeT]	The time expression.	required
subject_name	str	The subject name to bind to.	required

Returns:

Type	Description
TimeExpr[Any]	The bound expression.

Source code in src/guardrail_calculus/dimensions.py

def bind_time_expr(expr: TimeExpr[NodeT], *, subject_name: str) -> TimeExpr[Any]:
    """Bind subject-bound placeholders in a time expression.

    Args:
        expr: The time expression.
        subject_name: The subject name to bind to.

    Returns:
        The bound expression.
    """
    return _rebind_expr(expr, TimeExpr, subject_name=subject_name)

bind_duration_expr

bind_duration_expr(expr, *, subject_name)

Bind subject-bound placeholders in a duration expression.

Parameters:

Name	Type	Description	Default
expr	DurationExpr[NodeT]	The duration expression.	required
subject_name	str	The subject name to bind to.	required

Returns:

Type	Description
DurationExpr[Any]	The bound expression.

Source code in src/guardrail_calculus/dimensions.py

def bind_duration_expr(
    expr: DurationExpr[NodeT], *, subject_name: str
) -> DurationExpr[Any]:
    """Bind subject-bound placeholders in a duration expression.

    Args:
        expr: The duration expression.
        subject_name: The subject name to bind to.

    Returns:
        The bound expression.
    """
    return _rebind_expr(expr, DurationExpr, subject_name=subject_name)