# Copyright (C) 2023 IBM Corp.
# SPDX-License-Identifier: Apache-2.0
from abc import abstractmethod
from . import error, util
from .object import Object
__all__ = [
'Abstraction',
'Application',
'AtomicTerm',
'BoundVariable',
'CompoundTerm',
'Constant',
'Expression',
'Term',
'Type',
'TypeApplication',
'TypeConstructor',
'TypeVariable',
'Variable',
]
[docs]
class Expression(Object):
"""Abstract base class for expressions.
An :class:`Expression` can be either a :class:`Type` or a :class:`Term`.
Parameters:
args: Arguments
kwargs: Annotations.
Returns:
:class:`Expression`.
"""
__slots__ = (
'_cached_unfolded_args',
'_cached_type_constructors',
'_cached_type_variables',
)
def __neg__(self): # FIXME: generalize
return self.Not(self)
def __invert__(self): # FIXME: generalize
return self.Not(self)
def __and__(self, other): # FIXME: generalize
return self.And(self, other)
def __rand__(self, other): # FIXME: generalize
return self.And(other, self)
def __or__(self, other): # FIXME: generalize
return self.Or(self, other)
def __ror__(self, other): # FIXME: generalize
return self.Or(other, self)
def _build_unfolded_args_cache(self):
"""Gets the expression arguments unfolded."""
return tuple(self._get_unfolded_args_iterator())
def _get_unfolded_args_iterator(self): # defaults to args
return iter(self.args)
[docs]
def has_type_constructors(self):
"""Tests whether some type constructor occurs in expression.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.type_constructors)
def _build_type_constructors_cache(self):
"""Gets the set of type constructors occurring in expression."""
return frozenset(self._get_type_constructors_iterator())
@abstractmethod
def _get_type_constructors_iterator(self):
raise NotImplementedError
[docs]
def has_type_variables(self):
"""Tests whether some type variable occurs in expression.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.type_variables)
def _build_type_variables_cache(self):
"""Gets the set of type variables occurring in expression."""
return frozenset(self._get_type_variables_iterator())
@abstractmethod
def _get_type_variables_iterator(self):
raise NotImplementedError
[docs]
def instantiate(self, theta):
"""Applies type-variable instantiation `theta` to expression.
Parameters:
theta: Dictionary mapping type variables to types.
Returns:
The resulting :class:`Expression`.
.. code-block:: python
:caption: Example:
a, b = TypeVariables('a', 'b')
f = Constant('f', FunctionType(a, b))
x = Variable('x', a)
print(f(x))
# (f : a → b) (x : a)
print(f(x).instantiate({a: BaseType('nat'), b: BoolType()}))
# (f : nat → bool) (x : nat)
"""
return self._instantiate(theta)[0] if theta else self
@abstractmethod
def _instantiate(self, theta):
raise NotImplementedError
[docs]
class TypeConstructor(Expression):
"""Type constructor.
Type constructors are the building blocks of type expressions.
Parameters:
arg1: Id.
arg2: Arity.
arg3: Associativity (``'left'`` or ``'right'``).
kwargs: Annotations.
Returns:
A new :class:`TypeConstructor`.
"""
_associativity_values = {'left', 'right'}
def __init__( # (id, arity, associativity)
self, arg1, arg2, arg3=None, **kwargs):
super().__init__(arg1, arg2, arg3, **kwargs)
def _preprocess_arg(self, arg, i):
if i != 3: # skip possible None
arg = super()._preprocess_arg(arg, i)
if i == 1:
return self._preprocess_arg_id(self, arg, i)
elif i == 2:
return abs(error.check_arg_class(
arg, int, self.__class__.__name__, None, i))
elif i == 3:
return error.check_optional_arg_enum(
arg, self._associativity_values, None,
self.__class__.__name__, None, i)
else:
error.should_not_get_here()
def __call__(self, *args, **kwargs):
if self.associativity is None or len(args) <= self.arity:
return TypeApplication(self, *args, **kwargs)
elif self.associativity == 'left':
return util.foldl1(
lambda x, y: TypeApplication(self, x, y),
args).with_annotations(**kwargs)
elif self.associativity == 'right':
return util.foldr1(
lambda x, y: TypeApplication(self, x, y),
args).with_annotations(**kwargs)
else:
error.should_not_get_here()
@property
def id(self):
"""Type constructor id."""
return self.get_id()
def get_id(self):
"""Gets type constructor id.
Returns:
Type constructor id.
"""
return self[0]
@property
def arity(self):
"""Type constructor arity."""
return self.get_arity()
def get_arity(self):
"""Gets type constructor arity.
Returns:
Type constructor arity.
"""
return self[1]
@property
def associativity(self):
"""Type constructor associativity."""
return self.get_associativity()
def get_associativity(self):
"""Gets type constructor associativity.
Returns:
Type constructor associativity.
"""
return self[2]
def _get_type_constructors_iterator(self): # Expression
return iter([self])
def _get_type_variables_iterator(self): # Expression
return iter(())
def _instantiate(self, theta): # Expression
return self, False
[docs]
class Type(Expression):
"""Abstract base class for types.
A type is an expression representing a structured collection of values.
It can be either a :class:`TypeVariable` or a :class:`TypeApplication`.
"""
@staticmethod
def _preprocess_arg_type(self, arg, i):
if isinstance(arg, type):
try:
return self._thy().lookup_python_type_alias(arg)
except LookupError as err:
return error.arg_error(
arg, err, self.__class__.__name__, None, i)
else:
return Type.check(arg, self.__class__.__name__, None, i)
def match(self, other, theta=None):
"""Finds an instantiation that makes type match `other`.
Parameters:
other: :class:`Type`.
theta: Dictionary mapping variables to types.
Returns:
A type-variable instantiation (theta) if successful;
``None`` otherwise.
.. code-block:: python
:caption: Example:
a, b = TypeVariables('a', 'b')
t1 = FunctionType(a, b)
t2 = FunctionType(bool, bool, bool)
print(t1.match(t2))
# {(a : *): (bool : *), (b : *): (bool → bool : *)}
"""
other = Type.check(other, 'match', 'other', 1)
return self._match(other, theta or dict())
def matches(self, other):
"""Tests whether type can instantiated to match `other`.
Parameters:
other: :class:`Type`.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return self.match(other) is not None
@abstractmethod
def _match(self, other, theta):
raise NotImplementedError
[docs]
class TypeVariable(Type):
"""Type variable.
A type variable is an expression representing an arbitrary type.
Parameters:
arg1: Id.
kwargs: Annotations.
Returns:
A new :class:`TypeVariable`.
.. code-block:: python
:caption: Example:
a = TypeVariable('a')
print(a)
# a : *
See also:
:func:`TypeVariables`.
"""
def __init__( # (id,)
self, arg1, **kwargs):
super().__init__(arg1, **kwargs)
def _preprocess_arg(self, arg, i):
arg = super()._preprocess_arg(arg, i)
if i == 1:
return self._preprocess_arg_id(self, arg, i)
else:
error.should_not_get_here()
@property
def id(self):
"""Type variable id."""
return self.get_id()
def get_id(self):
"""Gets type variable id.
Returns:
Type variable id.
"""
return self[0]
def _get_type_constructors_iterator(self): # Expression
return iter(())
def _get_type_variables_iterator(self): # Expression
return iter([self])
def _instantiate(self, theta): # Expression
if self in theta:
return theta[self], True
else:
return self, False
def _match(self, other, theta): # Type
if self in theta:
return theta if theta[self] == other else None
else:
theta[self] = other
return theta
[docs]
class TypeApplication(Type):
"""Type application.
A type application is an expression representing the type obtained by
the application of a type constructor to other types.
Parameters:
arg1: :class:`TypeConstructor`.
args: :class:`Type`'s.
kwargs: Annotations.
Returns:
A new :class:`TypeApplication`.
.. code-block:: python
:caption: Example:
c0 = TypeConstructor('c0', 0)
print(c0()) # Equivalent to: TypeApplication(c0)
# c0 : *
c1 = TypeConstructor('c1', 1)
print(c1(c0())) # Equivalent to: TypeApplication(c1, c0())
# c1 c0 : *
"""
@classmethod
def _unfold(cls, arg):
tcons = arg.head
if tcons.arity == 2:
l, r = arg.tail
if tcons.associativity == 'left':
return tcons, *util.unfoldl(lambda x: x.tail if (
x.is_type_application()
and x.head == tcons) else None, arg)
elif tcons.associativity == 'right':
return tcons, *util.unfoldr(lambda x: x.tail if (
x.is_type_application()
and x.head == tcons) else None, arg)
return super()._unfold(arg)
def __init__( # (tcons, type, ..., type)
self, arg1, *args, **kwargs):
super().__init__(arg1, *args, **kwargs)
def _preprocess_args(self, args):
args = super()._preprocess_args(args)
tcons, exp, got = args[0], args[0].arity, len(args) - 1
if exp != got:
qtd = 'few' if got < exp else 'many'
error.arg_error(
tcons,
f'too {qtd} arguments: expected {exp}, got {got}',
self.__class__.__name__, None, 1)
return args
def _preprocess_arg(self, arg, i):
arg = super()._preprocess_arg(arg, i)
if i == 1:
return self._preprocess_arg_type_constructor(self, arg, i)
else:
return self._preprocess_arg_type(self, arg, i)
@property
def head(self):
"""Type application head.
.. code-block:: python
:caption: Example:
c0 = TypeConstructor('c0', 0)
c1 = TypeConstructor('c1', 1)
c2 = TypeConstructor('c2', 2)
print(c2(c1(c0()), c0()).head)
# c2
"""
return self.get_head()
def get_head(self):
"""Gets type application head.
Returns:
Type application head.
"""
return self[0]
@property
def tail(self):
"""Type application tail.
.. code-block:: python
:caption: Example:
c0 = TypeConstructor('c0', 0)
c1 = TypeConstructor('c1', 1)
c2 = TypeConstructor('c2', 2)
print(c2(c1(c0()), c0()).head)
# (c1 c0 : *, c0 : *)
"""
return self.get_tail()
def get_tail(self):
"""Gets type application tail.
Returns:
Type application tail.
"""
return self[1:]
def _get_unfolded_args_iterator(self): # Expression
return iter(self._unfold_type_application())
def _get_type_constructors_iterator(self): # Expression
return util.chain(
[self.head],
*map(lambda x: x.get_type_constructors(), self.tail))
def _get_type_variables_iterator(self): # Expression
return util.chain(
*map(lambda x: x.get_type_variables(), self.tail))
def _instantiate(self, theta): # Expression
args, status = [self.head], False
for x in self.tail:
y, s = x._instantiate(theta)
args.append(y)
status |= s
return self.with_args(*args), status
def _match(self, other, theta): # Type
if not other.is_type_application():
return None
h1, *t1 = self._unpack_type_application()
h2, *t2 = other._unpack_type_application()
if h1 != h2 or len(t1) != len(t2):
return None
for a, b in zip(t1, t2):
theta = a.match(b, theta)
if theta is None:
return None
return theta
[docs]
class Term(Expression):
"""Abstract base class for terms.
A term is an expression representing a value of a type.
It can be either a :class:`Variable`, :class:`Constant`,
:class:`Application`, or :class:`Abstraction`.
"""
__slots__ = (
'_cached_type',
'_cached_constants',
'_cached_variables',
'_cached_bound_variables',
'_cached_free_variables',
'_cached_nameless_variables',
)
@staticmethod
def _preprocess_arg_term(self, arg, i):
if not Term.test(arg):
try:
spec = self._thy().lookup_python_type_alias_spec(type(arg))
if hasattr(spec, 'cast'):
arg = spec.cast(arg)
except LookupError:
pass
return Term.check(arg, self.__class__.__name__, None, i)
def __call__(self, *args, **kwargs):
if (not args and self.is_atomic_term()
and not self.type.is_function_type()):
return self.with_annotations(**kwargs)
else:
return Application(self, *args, **kwargs)
def __rshift__(self, other):
return Abstraction(self, other)
def __rrshift__(self, other):
return Abstraction(*other, self)
def __lshift__(self, other):
return other >> self
def _build_type_cache(self):
"""Gets the term type."""
return self._get_type()
@abstractmethod
def _get_type(self):
raise NotImplementedError
def has_constants(self):
"""Tests whether some constant occurs in term.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.constants)
def _build_constants_cache(self):
"""Gets the set of constants occurring in term."""
return frozenset(self._get_constants_iterator())
@abstractmethod
def _get_constants_iterator(self):
raise NotImplementedError
def has_occurrence_of(self, x):
"""Tests whether variable `x` occurs (bound or free) in term.
Parameters:
x: :class:`Variable`.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return x in self.variables
def has_variables(self):
"""Tests whether some variable occurs in term.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.variables)
def _build_variables_cache(self):
"""Gets the set of variables occurring in term."""
return frozenset(self._get_variables_iterator())
@abstractmethod
def _get_variables_iterator(self):
raise NotImplementedError
def has_bound_occurrence_of(self, x):
"""Tests whether variable `x` occurs bound in term.
Parameters:
x: :class:`Variable`.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return x in self.bound_variables
def has_bound_variables(self):
"""Tests whether some bound variable occurs in term.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.bound_variables)
def _build_bound_variables_cache(self):
"""Gets the set of bound variables occurring in term."""
return frozenset(self._get_bound_variables_iterator())
@abstractmethod
def _get_bound_variables_iterator(self):
raise NotImplementedError
def has_free_occurrence_of(self, x):
"""Tests whether variable `x` occurs free in term.
Parameters:
x: :class:`Variable`.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return x in self.free_variables
def has_free_variables(self):
"""Tests whether some free variable occurs in term.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.free_variables)
def _build_free_variables_cache(self):
"""Gets the set of free variables occurring in term."""
return frozenset(self._get_free_variables_iterator())
@abstractmethod
def _get_free_variables_iterator(self):
raise NotImplementedError
def has_nameless_occurrence_of(self, x):
"""Tests whether nameless variable `x` occurs in term.
Parameters:
x: :class:`BoundVariable`.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return x in self.nameless_variables
def has_nameless_variables(self):
"""Tests whether some nameless variable occurs in term.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return bool(self.nameless_variables)
def _build_nameless_variables_cache(self):
"""Gets the set of nameless variables occurring in term."""
return frozenset(self._get_nameless_variables_iterator())
@abstractmethod
def _get_nameless_variables_iterator(self):
raise NotImplementedError
def open(self, x):
"""Replaces free variable `x` by bound variable in term.
(Internal: Not intended for direct use.)
Parameters:
x: :class:`Variable`.
Returns:
A new :class:`Term`.
.. code-block:: python
:caption: Example:
x, y = Variables('x', 'y', BoolType())
t = Abstraction(x, y)(y)
print(t.open(y))
# (𝜆 (x : bool) ⇒ (1 : bool)) (0 : bool)
See also:
:class:`BoundVariable`, :func:`Term.close`.
"""
return self._open(x, 0)
@abstractmethod
def _open(self, x, i):
raise NotImplementedError
def close(self, term):
"""Replaces bound variable by `term` in term.
(Internal: Not intended for direct use.)
Parameter:
term: :class:`Term`.
Returns:
A new :class:`Term`.
.. code-block:: python
:caption: Example:
x, y, z = Variables('x', 'y', 'z', BoolType())
t = Abstraction(x, y)(y)
t1 = t.open(y)
print(t1)
# (𝜆 (x : bool) ⇒ (1 : bool)) (0 : bool)
t2 = t1.close(z)
print(t2)
# (𝜆 (x : bool) ⇒ (z : bool)) (z : bool)
See also:
:class:`BoundVariable`, :func:`Term.open`.
"""
return self._close(term, 0)
@abstractmethod
def _close(self, term, i):
raise NotImplementedError
def substitute(self, theta):
"""Applies free-variable substitution `theta` to term.
Parameters:
theta: Dictionary mapping variables to terms.
Returns:
The resulting :class:`Term`.
Raises:
ValueError: `theta` is invalid.
.. code-block:: python
:caption: Example:
a = TypeVariable('a')
x, y, z = Variables('x', 'y', 'z', a)
f = Constant('f', FunctionType(a, a, a))
t = Abstraction(x, f(x, y))
print(t.substitute({y: z}))
# 𝜆 x ⇒ f x z
t = Abstraction(x, f(x, y))
print(t.substitute({y: x}))
# 𝜆 x0 ⇒ f x0 x
"""
for v, t in theta.items():
if not Variable.test(v) or not Term.test(t) or v.type != t.type:
return error.arg_error(
theta, 'invalid theta', 'substitute', 'theta', 1)
return self._substitute(theta)[0] if theta else self
@abstractmethod
def _substitute(self, theta):
raise NotImplementedError
class AtomicTerm(Term):
"""Abstract base class for atomic terms."""
@abstractmethod
def __init__( # (id, type)
self, arg1, type=None, **kwargs):
super().__init__(arg1, type, **kwargs)
def _preprocess_arg(self, arg, i):
if i == 1:
return self._preprocess_arg_id(self, arg, i)
elif i == 2:
return self._preprocess_arg_type(self, arg, i)
else:
error.should_not_get_here()
def __matmul__(self, kwargs):
if isinstance(kwargs, dict):
return super().__matmul__(kwargs)
else:
return self.with_type(
self._preprocess_arg_type(self, kwargs, 2))
@property
def id(self):
"""Atomic term id."""
return self.get_id()
def get_id(self):
"""Get atomic term id.
Returns:
Atomic term id.
"""
return self[0]
def _get_type_constructors_iterator(self): # Expression
return self.type.get_type_constructors()
def _get_type_variables_iterator(self): # Expression
return self.type.get_type_variables()
def _instantiate(self, theta): # Expression
type, status = self.type._instantiate(theta)
if status:
return self.with_type(type), True
else:
return self, False
def _get_type(self): # Term
return self[1]
def with_type(self, type):
"""Copies atomic term overwriting its type.
Parameters:
type: :class:`Type`.
Returns:
The resulting :class:`AtomicTerm`.
.. code-block:: python
:caption: Equivalent to:
term.copy(term.id, type)
"""
return self.with_args(self.id, type)
[docs]
class Variable(AtomicTerm):
"""Variable.
A variable is an atomic expression representing an arbitrary
value of a type.
Parameters:
arg1: Id.
type: :class:`Type`.
kwargs: Annotations.
Returns:
A new :class:`Variable`.
See also:
:func:`Variables`.
"""
def __init__( # (id, type)
self, arg1, type=None, **kwargs):
super().__init__(arg1, type=type, **kwargs)
def _get_constants_iterator(self): # Term
return iter(())
def _get_variables_iterator(self): # Term
return iter([self])
def _get_bound_variables_iterator(self): # Term
return iter(())
def _get_free_variables_iterator(self): # Term
return iter([self])
def _get_nameless_variables_iterator(self): # Term
return iter(())
def _open(self, x, i): # Term
if self.id == x.id and self.type == x.type:
return BoundVariable(i, self.type)
else:
return self
def _close(self, term, i): # Term
return self
def _substitute(self, theta): # Term
if self in theta:
return theta[self], True
else:
return self, False
def occurs_in(self, it):
"""Tests whether variable occurs in some term in `it`.
Parameters:
it: Iterable.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return util.any_map(lambda x: x.has_occurrence_of(self), iter(it))
def occurs_bound_in(self, it):
"""Tests whether variable occurs bound in some term in `it`.
Parameters:
it: Iterable.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return util.any_map(
lambda x: x.has_bound_occurrence_of(self), iter(it))
def occurs_free_in(self, it):
"""Tests whether variable occurs free in some term in `it`.
Parameters:
it: Iterable.
Returns:
``True`` if successful; ``False`` otherwise.
"""
return util.any_map(
lambda x: x.has_free_occurrence_of(self), iter(it))
def get_variant(self, avoid_test):
"""Gets a variant that passes `avoid_test`.
`avoid_test` is a function that takes a variable and returns
``True`` if it is unacceptable, or ``False`` if it is acceptable.
If variable passes `avoid_test`, returns variable itself.
Otherwise, generates and returns a similarly named variant that
passes `avoid_test`.
Parameter:
avoid_test: Function.
Returns:
Variable itself or a new similarly named variant.
.. code-block:: python
:caption: Example:
x = Variable('x', BoolType())
print(x.get_variant(lambda v: v == x))
# x : bool
print(x.get_variant(lambda v: v.id in {'x', 'x0', 'x1'}))
# x2 : bool
"""
x = self
while avoid_test(x):
x = x.with_args(util.get_variant(x.id), x.type)
return x
def get_variant_not_in(self, avoid):
"""Gets a variant that does not occur in `avoid`.
If variable does not occur in `avoid`, returns variable itself.
Otherwise, generates and returns a similarly named variant that does
not occur in `avoid`.
Parameters:
avoid: Iterable.
Returns:
Variable itself or a similarly named variant.
See also:
:func:`Variable.get_variable`.
"""
return self.get_variant(lambda x: x.occurs_in(avoid))
def get_variant_not_bound_in(self, avoid):
"""Gets a variant that does not occur bound in `avoid`.
If variable does not occur bound in `avoid`, returns variable
itself. Otherwise, generates and returns a similarly named variant
that does not occur bound in `avoid`.
Parameters:
avoid: Iterable.
Returns:
Variable itself or a similarly named variant.
See also:
:func:`Variable.get_variable`.
"""
return self.get_variant(lambda x: x.occurs_bound_in(avoid))
def get_variant_not_free_in(self, avoid):
"""Gets a variant that does not occur free in `avoid`.
If variable does not occur free in `avoid`, returns variable itself.
Otherwise, generates and returns a similarly named variant that does
not occur free in `avoid`.
Parameters:
avoid: Iterable.
Returns:
Variable itself or a similarly named variant.
See also:
:func:`Variable.get_variable`.
"""
return self.get_variant(lambda x: x.occurs_free_in(avoid))
[docs]
class BoundVariable(Variable):
"""Bound variable.
(Internal: Not intended for direct use.)
Internally, terms use what is called a `locally nameless representation`.
This is a combination of using De Bruijn indices for variables local to
the current term (:class:`BoundVariable`) and names for variables global
to the current term (:class:`Variable`). See C. McBride and J. McKinna,
"Functional Pearl: I am not a number--I am a free variable", Haskell'04,
2004. ACM.
See also:
:func:`Term.open`, :func:`Term.close`.
"""
def __init__( # (id, type)
self, arg1, type=None, **kwargs):
super().__init__(arg1, type=type, **kwargs)
def _preprocess_arg(self, arg, i):
arg = super()._preprocess_arg(arg, i)
if i == 1:
return error.check_arg_class(
arg, int, self.__class__.__name__, None, i)
elif i == 2:
return arg
else:
error.should_not_get_here()
def _get_constants_iterator(self): # Term
return iter(())
def _get_variables_iterator(self): # Term
return iter(())
def _get_bound_variables_iterator(self): # Term
return iter(())
def _get_free_variables_iterator(self): # Term
return iter(())
def _get_nameless_variables_iterator(self): # Term
return iter([self])
def _open(self, x, i): # Term
return self
def _close(self, term, i): # Term
if self.id == i and self.type == term.type:
return term
else:
return self
def _substitute(self, theta): # Term
return self, False
def occurs_in(self, it): # Variable
error.should_not_get_here()
def occurs_bound_in(self, it): # Variable
error.should_not_get_here()
def occurs_free_in(self, it): # Variable
error.should_not_get_here()
def get_variant(self, avoid_test): # Variable
error.should_not_get_here()
def get_variant_not_in(self, avoid): # Variable
error.should_not_get_here()
def get_variant_not_bound_in(self, avoid): # Variable
error.should_not_get_here()
def get_variant_not_free_in(self, avoid): # Variable
error.should_not_get_here()
[docs]
class Constant(AtomicTerm):
"""Constant.
A constant is an atomic expression representing a particular
value of a type.
Parameters:
arg1: Id.
type: :class:`Type`.
kwargs: Annotations.
Returns:
A new :class:`Constant`.
See also:
:func:`Constants`.
"""
def __init__( # (id, type)
self, arg1, type=None, **kwargs):
super().__init__(arg1, type=type, **kwargs)
def _get_constants_iterator(self): # Term
return iter([self])
def _get_variables_iterator(self): # Term
return iter(())
def _get_bound_variables_iterator(self): # Term
return iter(())
def _get_free_variables_iterator(self): # Term
return iter(())
def _get_nameless_variables_iterator(self): # Term
return iter(())
def _open(self, x, i): # Term
return self
def _close(self, term, i): # Term
return self
def _substitute(self, theta): # Term
return self, False
class CompoundTerm(Term):
"""Abstract base class for compound terms."""
@property
def left(self):
"""First argument of compound term."""
return self.get_left()
def get_left(self):
"""Gets the first argument of compound term.
Returns:
First argument of compound term.
"""
return self[0]
@property
def right(self):
"""Second argument of compound term."""
return self.get_right()
def get_right(self):
"""Gets the second argument of compound term.
Returns:
Second argument of compound term."""
return self[1]
def _get_type_variables_iterator(self): # Expression
return util.chain(
self[0].get_type_variables(),
self[1].get_type_variables())
[docs]
class Application(CompoundTerm):
"""Application.
An application is a compound expression representing the application
of `arg1` to `arg2`.
Application is left-associative: If more than two arguments are given,
the result is left-folded.
Parameters:
arg1: :class:`Term`.
arg2: :class:`Term`.
args: Remaining :class:`Term`'s.
kwargs: Annotations.
Returns:
A new :class:`Application`.
Raises:
ValueError: `arg1` cannot be applied to `arg2`.
"""
@classmethod
def _unfold(cls, arg):
return tuple(util.unfoldl(
Application.unpack_application_unsafe, arg))
def __init__( # (term1, term2, ...)
self, arg1, arg2, *args, **kwargs):
util.foldl_infix(
super().__init__, self.__class__, arg1, arg2, *args, **kwargs)
def _preprocess_arg(self, arg, i):
arg = super()._preprocess_arg(arg, i)
arg = self._preprocess_arg_term(self, arg, i)
if i == 1:
return error.check_arg(
arg, arg.type.test_function_type(), 'not a function',
self.__class__.__name__, None, i)
elif i == 2:
return arg
else:
error.should_not_get_here()
def _preprocess_args(self, args):
args = super()._preprocess_args(args)
dom, _ = args[0].type.unpack_function_type()
got = args[1].type
theta = dom.match(got)
if theta is None:
error.arg_error(
args[1], f"expected '{dom}', got '{got}'",
self.__class__.__name__, None, 1)
elif theta:
return args[0].instantiate(theta), args[1]
return args
def _get_unfolded_args_iterator(self): # Expression
return iter(self._unfold_application())
def _get_type_constructors_iterator(self): # Expression
return util.chain(
self[0].get_type_constructors(),
self[1].get_type_constructors())
def _instantiate(self, theta): # Expression
left, lstatus = self[0]._instantiate(theta)
right, rstatus = self[1]._instantiate(theta)
if lstatus or rstatus:
return self.with_args(left, right), True
else:
return self, False
def _get_type(self): # Term
return self[0].type[2]
def _get_constants_iterator(self): # Term
return util.chain(
self[0].get_constants(),
self[1].get_constants())
def _get_variables_iterator(self): # Term
return util.chain(
self[0].get_variables(),
self[1].get_variables())
def _get_bound_variables_iterator(self): # Term
return util.chain(
self[0].get_bound_variables(),
self[1].get_bound_variables())
def _get_free_variables_iterator(self): # Term
return util.chain(
self[0].get_free_variables(),
self[1].get_free_variables())
def _get_nameless_variables_iterator(self): # Term
return util.chain(
self[0].get_nameless_variables(),
self[1].get_nameless_variables())
def _open(self, x, i): # Term
freel = self[0].has_free_occurrence_of(x)
freer = self[1].has_free_occurrence_of(x)
if freel and freer:
return self.with_args(
self[0]._open(x, i), self[1]._open(x, i))
elif freel:
return self.with_args(self[0]._open(x, i), self[1])
elif freer:
return self.with_args(self[0], self[1]._open(x, i))
else:
return self
def _close(self, term, i, _nty=Term.get_type): # Term
lessl = term.type in map(_nty, self[0].nameless_variables)
lessr = term.type in map(_nty, self[1].nameless_variables)
if lessl and lessr:
return self.with_args(
self[0]._close(term, i), self[1]._close(term, i))
elif lessl:
return self.with_args(self[0]._close(term, i), self[1])
elif lessr:
return self.with_args(self[0], self[1]._close(term, i))
else:
return self
def _substitute(self, theta): # Term
left, lstatus = self[0]._substitute(theta)
right, rstatus = self[1]._substitute(theta)
if lstatus or rstatus:
return self.with_args(left, right), True
else:
return self, False
[docs]
class Abstraction(CompoundTerm):
"""Abstraction.
An abstraction is a compound expression representing the function
obtained by abstracting variable `arg1` over `arg2`.
Abstraction is right-associative: If more than two arguments are given,
the result is right-folded.
Parameters:
arg1: :class:`Variable`.
arg2: :class:`Variable` or :class:`Term`.
args: Remaining :class:`Variable`'s followed by a :class:`Term`.
_open: Whether to open `arg1` in `arg2`.
(Internal: Not intended for direct use.)
kwargs: Annotations.
Returns:
A new :class:`Abstraction`.
"""
@classmethod
def _dup(cls, *args, **kwargs):
return cls(*args, _open=False, **kwargs)
@classmethod
def _unfold(cls, arg):
return tuple(util.unfoldr(
Abstraction.unpack_abstraction_unsafe, arg))
@classmethod
def _unpack(cls, arg):
return arg.left, arg.right
__slots__ = (
'_cached_undebruijned_args',
)
def __init__( # (var1, var2, ..., term)
self, arg1, arg2, *args, _open=True, **kwargs):
self._open_flag = _open # hack to pass _open to _preprocess_args;
if not args: # we can't use util.foldr_infix below
super().__init__(arg1, arg2, **kwargs)
else:
arg2 = self.__class__(arg2, *args, _open=_open)
return super().__init__(arg1, arg2, **kwargs)
def __eq__(self, other): # anonymize arg[0]
return (type(self) == type(other)
and self[0].type == other[0].type
and self[1] == other[1])
def __hash__(self): # anonymize arg[0]
return hash((self.__class__, self[0].type, self[1]))
def _dump(self): # anonymize arg[0]
cls_name = self.__class__.__name__
return f'({cls_name} {self[0].type.dump()} {self[1].dump()})'
def _preprocess_arg(self, arg, i, **kwargs):
arg = super()._preprocess_arg(arg, i)
if i == 1:
return self._preprocess_arg_variable(self, arg, i)
elif i == 2:
return self._preprocess_arg_term(self, arg, i)
else:
error.should_not_get_here()
def _preprocess_args(self, args):
args = super()._preprocess_args(args)
open_flag = self._open_flag
delattr(self, '_open_flag')
if open_flag:
return args[0], args[1].open(args[0])
else:
return args
def _get_unfolded_args_iterator(self): # Expression
return iter(self._unfold_abstraction())
def _get_type_constructors_iterator(self): # Expression
return util.chain(
[self.type.head],
self[0].get_type_constructors(),
self[1].get_type_constructors())
def _instantiate(self, theta): # Expression
left, lstatus = self[0]._instantiate(theta)
right, rstatus = self[1]._instantiate(theta)
if not lstatus and not rstatus:
return self, False
if left.occurs_free_in([right]):
left = left.get_variant_not_free_in([right])
return self.with_args(left, right), True
def _get_type(self): # Term
return self.FunctionType(self[0].type, self[1].type)
def _get_constants_iterator(self): # Term
return iter(self[1].get_constants())
def _get_variables_iterator(self): # Term
return util.chain([self[0]], self[1].get_variables())
def _get_bound_variables_iterator(self): # Term
return util.chain([self[0]], self[1].get_bound_variables())
def _get_free_variables_iterator(self): # Term
return iter(self[1].get_free_variables())
def _get_nameless_variables_iterator(self): # Term
return iter(self[1].get_nameless_variables())
def _open(self, x, i): # Term
if not self[1].has_free_occurrence_of(x):
return self
else:
return self.with_args(self[0], self[1]._open(x, i + 1))
def _close(self, term, i, _nty=Term.get_type): # Term
if term.type not in map(_nty, self[1].nameless_variables):
return self
else:
return self.with_args(self[0], self[1]._close(term, i + 1))
def _substitute(self, theta):
left = self[0]
right, rstatus = self[1]._substitute(theta)
if not rstatus:
return self, False
if left.occurs_in([right]): # rename
left = left.get_variant_not_in([right])
return self.with_args(left, right), True
def get_right(self): # CompoundTerm
return self.undebruijned_args[1]
def _build_undebruijned_args_cache(self):
"""Gets the arguments of abstraction un-De Bruijn'ed."""
return self[0], self[1].close(self[0])
def rename(self, x):
"""Renames bound variable to `x`.
If `x` occurs free in the abstraction, instead of `x` uses its first
variant not free in the abstraction.
Parameters:
x: :class:`Variable`.
Returns:
A new :class:`Abstraction`.
See also:
:func:`Variable.get_variant_not_free_in`.
"""
if x == self[0]:
return self
else:
if x.occurs_in([self[1]]):
x = x.get_variant_not_in([self[1]])
return self.with_args(x, self[1])