improve docstrings of package visitors.substitution

Author: Deric-W

lambda_calculus/visitors/__init__.py

@@ -167,7 +167,7 @@ def defer_application(self, application: terms.Application[V]) -> tuple[T, Defer
         """
         Visit an Application term.
 
-        :param abstraction: application term to visit
+        :param application: application term to visit
         :return: tuple containing a value as required by its type variable
                  and visitors to be used for visiting its abstraction and argument
         """

lambda_calculus/visitors/substitution/__init__.py

@@ -20,45 +20,92 @@
 
 
 class Substitution(Visitor["terms.Term[V]", V]):
-    """ABC for Visitors which replace a free Variable with another term"""
+    """
+    ABC for Visitors which replace a free Variable with another term.
+
+    Type Variables:
+
+        V: represents the type of variables used in terms
+    """
 
     __slots__ = ()
 
     @abstractmethod
     def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> terms.Abstraction[V]:
-        """visit an Abstraction term"""
+        """
+        Visit an Abstraction term
+
+        The body is not automatically visited.
+
+        :param abstraction: abstraction term to visit
+        :return: new term with substitutions performed
+        """
         raise NotImplementedError()
 
     @abstractmethod
     def visit_application(self, application: terms.Application[V]) -> terms.Application[V]:
-        """visit an Application term"""
+        """
+        Visit an Application term
+
+        The abstraction and argument are not automatically visited.
+
+        :param appliation: application term to visit
+        :return: new term with substitutions performed
+        """
         raise NotImplementedError()
 
     @classmethod
     @abstractmethod
     def from_substitution(cls: Type[T], variable: V, value: terms.Term[V]) -> T:
-        """create an instance from the substitution it should perform"""
+        """
+        Create an instance from the substitution it should perform
+
+        :param variable: variable to substitute
+        :param value: value which should be substituted
+        :return: new instance
+        """
         raise NotImplementedError()
 
 
 class DeferrableSubstitution(DeferrableVisitor["terms.Term[V]", V], Substitution[V]):
-    """ABC for Substitutions which can be performed lazyly"""
+    """
+    ABC for Substitutions which can be performed lazyly.
+    """
 
     __slots__ = ()
 
     @abstractmethod
     def defer_abstraction(self, abstraction: terms.Abstraction[V]) -> tuple[terms.Abstraction[V], DeferrableSubstitution[V] | None]:
-        """visit an Abstraction term and return the visitor used to visit its body"""
+        """
+        Visit an Abstraction term.
+
+        :param abstraction: abstraction term to visit
+        :return: tuple containing a new term instance with substitutions performed
+                 and a visitor to be used for visiting its body
+        """
         raise NotImplementedError()
 
     @abstractmethod
     def defer_application(self, application: terms.Application[V]) -> tuple[terms.Application[V], DeferrableSubstitution[V] | None, DeferrableSubstitution[V] | None]:
-        """visit an Application term and return the visitors used to visit its abstraction and argument"""
+        """
+        Visit an Application term.
+
+        :param application: application term to visit
+        :return: tuple containing a new term instance with substitutions performed
+                 and visitors to be used for visiting its abstraction and argument
+        """
         raise NotImplementedError()
 
     @final
     def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> terms.Abstraction[V]:
-        """visit an Abstraction term"""
+        """
+        Visit an Abstraction term
+
+        The body is visited after performing substitution.
+
+        :param abstraction: abstraction term to visit
+        :return: new term instance with substitutions performed
+        """
         substituted, body_visitor = self.defer_abstraction(abstraction)
         if body_visitor is None:
             return substituted
@@ -69,7 +116,14 @@ def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> terms.Abstract
 
     @final
     def visit_application(self, application: terms.Application[V]) -> terms.Application[V]:
-        """visit an Application term"""
+        """
+        Visit an Application term
+
+        The abstraction and argument are visited after performing substitution.
+
+        :param appliation: application term to visit
+        :return: new term instance with substitutions performed
+        """
         substituted, abstraction_visitor, argument_visitor = self.defer_application(application)
         if abstraction_visitor is None:
             abstraction = substituted.abstraction

lambda_calculus/visitors/substitution/checked.py

@@ -19,8 +19,12 @@
 @final
 class CheckedSubstitution(Substitution[V]):
     """
-    Visitor which replaces a free Variable with another term
-    Raises a CollisionError if a free variable gets bound
+    Substitution which checks if a free variable gets bound.
+
+    :param variable: variable to substitute
+    :param value: value which should be substituted
+    :param free_variables: free variables which should not be bound
+    :raise errors.CollisionError: If a free variable gets bound
     """
 
     variable: V
@@ -47,23 +51,50 @@ def __init__(self, variable: V, value: terms.Term[V], free_variables: Set[V]) ->
 
     @classmethod
     def from_substitution(cls, variable: V, value: terms.Term[V]) -> CheckedSubstitution[V]:
-        """create an instance from the substitution it should perform"""
+        """
+        Create an instance from the substitution it should perform
+
+        :param variable: variable to substitute
+        :param value: value which should be substituted
+        :return: new instance with free_variables set to the free variables of value
+        """
         return cls(variable, value, value.free_variables())
 
     def bind_variable(self, name: V) -> None:
-        """mark a variable as bound"""
+        """
+        Mark a variable as bound.
+
+        Bound variables are not automatically unbound
+        and can be bound multiple times.
+
+        :param name: name of the variable
+        """
         self.bound_variables[name] = self.bound_variables.get(name, 0) + 1
 
     def unbind_variable(self, name: V) -> None:
-        """mark a variable as not bound"""
+        """
+        Mark a variable as not bound.
+
+        A variable needs to be unbound multiple times
+        if it was bound multiple times.
+
+        :param name: name of the variable
+        :raise KeyError: If the variable is not bound
+        """
         number = self.bound_variables[name]
         if number == 1:
             del self.bound_variables[name]
         else:
             self.bound_variables[name] = number - 1
 
     def visit_variable(self, variable: terms.Variable[V]) -> terms.Term[V]:
-        """visit a Variable term"""
+        """
+        Visit a Variable term.
+
+        :param variable: variable term to visit
+        :raise errors.CollisionError: If the substitution whould bind free variables
+        :return: variable term or value which should be substituted
+        """
         if variable.name != self.variable:
             return variable
         collisions = self.free_variables & self.bound_variables.keys()
@@ -72,7 +103,14 @@ def visit_variable(self, variable: terms.Variable[V]) -> terms.Term[V]:
         return self.value
 
     def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> terms.Abstraction[V]:
-        """visit an Abstraction term"""
+        """
+        Visit an Abstraction term.
+
+        :param abstraction: abstraction term to visit
+        :raise errors.CollisionError: If a substitution in the body
+                                      whould bind free variables
+        :return: abstraction term or new term with substitutions performed
+        """
         if abstraction.bound == self.variable:
             return abstraction
         self.bind_variable(abstraction.bound)
@@ -86,7 +124,14 @@ def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> terms.Abstract
             self.unbind_variable(abstraction.bound)
 
     def visit_application(self, application: terms.Application[V]) -> terms.Application[V]:
-        """visit an Application term"""
+        """
+        Visit an Application term.
+
+        :param appliation: application term to visit
+        :raise errors.CollisionError: If a substitution in the abstraction
+                                      or argument whould bind free variables
+        :return: new term with substitutions performed
+        """
         return terms.Application(
             application.abstraction.accept(self),
             application.argument.accept(self)

lambda_calculus/visitors/substitution/renaming.py

@@ -23,8 +23,8 @@
 
 class RenamingSubstitution(DeferrableSubstitution[V]):
     """
-    Visitor which replaces a free Variable with another term
-    Renames bound variables if a free variable gets bound
+    ABC for Substitutions which rename
+    bound variables if a free variable gets bound.
     """
 
     variable: V
@@ -38,39 +38,67 @@ class RenamingSubstitution(DeferrableSubstitution[V]):
 
     @abstractmethod
     def prevent_collision(self, abstraction: terms.Abstraction[V]) -> terms.Abstraction[V]:
-        """prevent collisions by renaming bound variables"""
+        """
+        Prevent collisions by renaming bound variables.
+
+        :param abstraction: abstraction term which could bind free variables
+        :return: abstraction term which does not bind free variables
+        """
         raise NotImplementedError()
 
     @final
     def trace(self) -> TracingDecorator[V]:
-        """return a new visitor which yields when an alpha conversion occurs"""
+        """
+        Create a new visitor which yields when an alpha conversion occurs.
+
+        :return: new visitor wrapping this instance
+        """
         return TracingDecorator(self)
 
     @final
     def visit_variable(self, variable: terms.Variable[V]) -> terms.Term[V]:
-        """visit a Variable term"""
+        """
+        Visit a Variable term.
+
+        :param variable: variable term to visit
+        :return: variable term or value which should be substituted
+        """
         if variable.name != self.variable:
             return variable
         return self.value
 
     @final
     def defer_abstraction(self, abstraction: terms.Abstraction[V]) -> tuple[terms.Abstraction[V], RenamingSubstitution[V] | None]:
-        """visit an Abstraction term and return the visitor used to visit its body"""
+        """
+        Visit an Abstraction term.
+
+        :param abstraction: abstraction term to visit
+        :return: tuple containing an abstraction term not binding free variables and
+                 this visitor to be used for visiting its body if variable is not bound
+        """
         if abstraction.bound == self.variable:
             return abstraction, None
         return self.prevent_collision(abstraction), self
 
     @final
     def defer_application(self, application: terms.Application[V]) -> tuple[terms.Application[V], RenamingSubstitution[V], RenamingSubstitution[V]]:
-        """visit an Application term and return the visitors used to visit its abstraction and argument"""
+        """
+        Visit an Application term.
+
+        :param application: application term to visit
+        :return: tuple containing the application term and this visitor
+                 to be used for visiting its abstraction and argument
+        """
         return application, self, self
 
 
 @final
 class TracingDecorator(Visitor[Generator["terms.Term[V]", None, "terms.Term[V]"], V]):
     """
-    Visitor which transforms a RenamingSubstitution into an Generator
-    which yields after performing an alpha conversion
+    Visitor which transforms a :class:`RenamingSubstitution` into an Generator
+    which yields after performing an alpha conversion and returns the term with substitutions.
+
+    :param substitution: instance to wrap
     """
 
     substitution: RenamingSubstitution[V]
@@ -81,13 +109,25 @@ def __init__(self, substitution: RenamingSubstitution[V]) -> None:
         self.substitution = substitution
 
     def visit_variable(self, variable: terms.Variable[V]) -> Generator[terms.Variable[V], None, terms.Term[V]]:
-        """visit a Variable term"""
+        """
+        Visit a Variable term.
+
+        :param variable: variable term to visit
+        :return: empty Generator returning the result
+                 of :meth:`RenamingSubstitution.visit_variable`
+        """
         return self.substitution.visit_variable(variable)
         # to create a generator
         yield variable  # type: ignore[unreachable]
 
     def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> Generator[terms.Abstraction[V], None, terms.Abstraction[V]]:
-        """visit an Abstraction term"""
+        """
+        Visit an Abstraction term
+
+        :param abstraction: abstraction term to visit
+        :return: Generator yielding alpha conversions and
+                 returning the term with substitutions
+        """
         substituted, visitor = self.substitution.defer_abstraction(abstraction)
         if visitor is None:
             return substituted
@@ -98,7 +138,13 @@ def visit_abstraction(self, abstraction: terms.Abstraction[V]) -> Generator[term
         return terms.Abstraction(substituted.bound, body)
 
     def visit_application(self, application: terms.Application[V]) -> Generator[terms.Application[V], None, terms.Application[V]]:
-        """visit an Application term"""
+        """
+        Visit an Application term
+
+        :param appliation: application term to visit
+        :return: Generator yielding alpha conversions and
+                 returning the term with substitutions
+        """
         # distinguish between last alpha conversion (step) and
         # substituted abstraction (abstraction)
         abstraction = step = application.abstraction
@@ -119,8 +165,12 @@ def visit_application(self, application: terms.Application[V]) -> Generator[term
 @final
 class CountingSubstitution(RenamingSubstitution[str]):
     """
-    Visitor which replaces a free Variable with another term
-    Renames bound variables if a free variable gets bound by appending a number
+    Substitution which renames bound variables
+    if a free variable gets bound by appending a number.
+
+    :param variable: variable to substitute
+    :param value: value which should be substituted
+    :param free_variables: free variables which should not be bound
     """
 
     free_variables: Set[str]
@@ -134,11 +184,22 @@ def __init__(self, variable: str, value: terms.Term[str], free_variables: Set[st
 
     @classmethod
     def from_substitution(cls, variable: str, value: terms.Term[str]) -> CountingSubstitution:
-        """create an instance from the substitution it should perform"""
+        """
+        Create an instance from the substitution it should perform
+
+        :param variable: variable to substitute
+        :param value: value which should be substituted
+        :return: new instance with free_variables set to the free variables of value
+        """
         return cls(variable, value, value.free_variables())
 
     def prevent_collision(self, abstraction: terms.Abstraction[str]) -> terms.Abstraction[str]:
-        """prevent collisions by renaming bound variables"""
+        """
+        Prevent collisions by appending a number.
+
+        :param abstraction: abstraction term which could bind free variables
+        :return: abstraction term which does not bind free variables
+        """
         if abstraction.bound in self.free_variables:
             used_variables = abstraction.body.bound_variables() \
                 | abstraction.free_variables() \