Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions pyds/__init__.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
"""Python wrapper for a deductive system implemented in C++.

Provides classes and functions for working with logical terms, rules, and inference.
"""

__all__ = [
"buffer_size",
"scoped_buffer_size",
Expand Down
30 changes: 30 additions & 0 deletions pyds/buffer_size.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
"""Buffer size management for the deductive system."""

__all__ = [
"buffer_size",
"scoped_buffer_size",
Expand All @@ -9,6 +11,20 @@


def buffer_size(size: int = 0) -> int:
"""Gets the current buffer size, or sets a new buffer size and returns the previous value.

The buffer size is used for internal operations like conversions and transformations.

Args:
size: The new buffer size to set. If 0 (default), the current size is returned without modification.

Returns:
The previous buffer size value.

Example:
>>> current_size = buffer_size() # Get current size
>>> old_size = buffer_size(2048) # Set new size, returns old size
"""
global _buffer_size
old_buffer_size = _buffer_size
if size > 0:
Expand All @@ -18,6 +34,20 @@ def buffer_size(size: int = 0) -> int:

@contextmanager
def scoped_buffer_size(size: int = 0):
"""Context manager for temporarily changing the buffer size.

Sets the buffer size for the duration of the context and restores the
previous value when exiting.

Args:
size: The temporary buffer size to set.

Example:
>>> with scoped_buffer_size(4096):
... # Operations here use buffer size of 4096
... pass
>>> # Buffer size is restored to previous value
"""
old_buffer_size = buffer_size(size)
try:
yield
Expand Down
40 changes: 40 additions & 0 deletions pyds/common.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
"""Base class for all deductive system wrapper types."""

from __future__ import annotations

__all__ = [
Expand All @@ -11,9 +13,24 @@


class Common(typing.Generic[T]):
"""Base class for all deductive system wrapper types.

Handles initialization, serialization, and common operations.
"""

_base: type[T]

def __init__(self, value: Common[T] | T | str | bytes, size: int | None = None) -> None:
"""Creates a new instance.

Args:
value: Initial value (can be another instance, base value, string, or memoryview).
size: Optional buffer capacity for the internal storage.

Raises:
ValueError: If initialization fails or invalid arguments are provided.
TypeError: If value is of an unsupported type.
"""
self.value: T
self.capacity: int | None
if isinstance(value, type(self)):
Expand All @@ -38,6 +55,14 @@ def __init__(self, value: Common[T] | T | str | bytes, size: int | None = None)
raise TypeError("Unsupported type for initialization.")

def __str__(self) -> str:
"""Convert the value to a string representation.

Returns:
The string representation.

Raises:
ValueError: If conversion fails.
"""
result = self._base.to_string(self.value, buffer_size())
if result == "":
raise ValueError("Conversion to string failed.")
Expand All @@ -47,12 +72,27 @@ def __repr__(self) -> str:
return f"{type(self).__name__}[{self}]"

def data(self) -> bytes:
"""Get the binary representation of the value.

Returns:
The binary data as bytes.
"""
return self._base.to_binary(self.value)

def size(self) -> int:
"""Get the size of the data in bytes.

Returns:
The data size.
"""
return self.value.data_size()

def __copy__(self) -> Common[T]:
"""Create a deep copy of this instance.

Returns:
A new instance with cloned value.
"""
return type(self)(self.value.clone(), self.size())

def __hash__(self) -> int:
Expand Down
16 changes: 16 additions & 0 deletions pyds/item_t.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
"""Wrapper class for items in the deductive system."""

__all__ = [
"Item",
]
Expand All @@ -8,8 +10,22 @@


class Item(Common[ds.Item]):
"""Wrapper class for items in the deductive system.

Items represent constants or functors in logical terms.

Example:
>>> item = Item("atom")
>>> print(item.name) # "atom"
"""

_base = ds.Item

@property
def name(self) -> String:
"""Get the name of this item.

Returns:
The item name as a String.
"""
return String(self.value.name())
25 changes: 25 additions & 0 deletions pyds/list_t.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
"""Wrapper class for lists in the deductive system."""

from __future__ import annotations

__all__ = [
Expand All @@ -13,12 +15,35 @@


class List(Common[ds.List]):
"""Wrapper class for lists in the deductive system.

Lists contain ordered sequences of terms.

Example:
>>> lst = List("(a b c)")
>>> print(len(lst)) # 3
>>> print(lst[0]) # "a"
"""

_base = ds.List

def __len__(self) -> int:
"""Get the number of elements in the list.

Returns:
The list length.
"""
return len(self.value)

def __getitem__(self, index: int) -> Term:
"""Get an element from the list by index.

Args:
index: The zero-based index of the element.

Returns:
The term at the specified index.
"""
from .term_t import Term

return Term(self.value[index])
71 changes: 71 additions & 0 deletions pyds/rule_t.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
"""Wrapper class for logical rules in the deductive system."""

from __future__ import annotations

__all__ = [
Expand All @@ -11,29 +13,98 @@


class Rule(Common[ds.Rule]):
"""Wrapper class for logical rules in the deductive system.

A rule consists of zero or more premises (above the line) and a conclusion (below the line).

Example:
>>> rule = Rule("(father `X `Y)\\n----------\\n(parent `X `Y)\\n")
>>> print(rule.conclusion) # "(parent `X `Y)"
>>> print(len(rule)) # 1 (number of premises)
"""

_base = ds.Rule

def __len__(self) -> int:
"""Get the number of premises in the rule.

Returns:
The number of premises.
"""
return len(self.value)

def __getitem__(self, index: int) -> Term:
"""Get a premise term by index.

Args:
index: The zero-based index of the premise.

Returns:
The premise term at the specified index.
"""
return Term(self.value[index])

@property
def conclusion(self) -> Term:
"""Get the conclusion of the rule.

Returns:
The conclusion term.
"""
return Term(self.value.conclusion())

def __floordiv__(self, other: Rule) -> Rule | None:
return self.ground(other)

def ground(self, other: Rule, scope: str | None = None) -> Rule | None:
"""Ground this rule using a dictionary to substitute variables with values.

Args:
other: A rule representing a dictionary (list of pairs). Each pair contains
a variable and its substitution value.
Example: Rule("((`a b))") means substitute variable `a with value b.
scope: Optional scope string for variable scoping.

Returns:
The grounded rule, or None if grounding fails.

Example:
>>> a = Rule("`a")
>>> b = Rule("((`a b))")
>>> str(a.ground(b))
'----\\nb\\n'
>>>
>>> # With scope
>>> c = Rule("`a")
>>> d = Rule("((x y `a `b) (y x `b `c))")
>>> str(c.ground(d, "x"))
'----\\n`c\\n'
"""
capacity = buffer_size()
rule = ds.Rule.ground(self.value, other.value, scope, capacity)
if rule is None:
return None
return Rule(rule, capacity)

def __matmul__(self, other: Rule) -> Rule | None:
"""Match this rule with another rule using unification.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

这个缺少了例子啊, js那边好像是有例子的

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

已添加例子到 __matmul__ 方法的docstring中,参考了TypeScript版本的match方法例子。改动已在提交 4bc992c 中。


This is the operator form of the match method, using the @ operator.
This unifies the first premise of this rule with the other rule.
The other rule must be a fact (a rule without premises).

Args:
other: The rule to match against (must be a fact without premises).

Returns:
The matched rule, or None if matching fails.

Example:
>>> mp = Rule("(`p -> `q)\\n`p\\n`q\\n")
>>> pq = Rule("((! (! `x)) -> `x)")
>>> str(mp @ pq)
'(! (! `x))\\n----------\\n`x\\n'
"""
capacity = buffer_size()
rule = ds.Rule.match(self.value, other.value, capacity)
if rule is None:
Expand Down
52 changes: 52 additions & 0 deletions pyds/search_t.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
"""Search engine for the deductive system."""

__all__ = [
"Search",
]
Expand All @@ -8,20 +10,70 @@


class Search:
"""Search engine for the deductive system.

Manages a knowledge base of rules and performs logical inference.

Example:
>>> search = Search()
>>> search.add("(parent john mary)")
>>> search.add("(father `X `Y)\\n----------\\n(parent `X `Y)\\n")
>>> def callback(rule):
... print(rule)
... return False # Return False to continue, True to stop
>>> search.execute(callback)
"""

def __init__(self, limit_size: int = 1000, buffer_size: int = 10000):
"""Creates a new search engine instance.

Args:
limit_size: Size of the buffer for storing the final objects (rules/facts)
in the knowledge base (default: 1000).
buffer_size: Size of the buffer for internal operations like conversions
and transformations (default: 10000).
"""
self._search: ds.Search = ds.Search(limit_size, buffer_size)

def set_limit_size(self, limit_size: int) -> None:
"""Set the size of the buffer for storing final objects.

Args:
limit_size: The new limit size for storing rules/facts.
"""
self._search.set_limit_size(limit_size)

def set_buffer_size(self, buffer_size: int) -> None:
"""Set the buffer size for internal operations.

Args:
buffer_size: The new buffer size.
"""
self._search.set_buffer_size(buffer_size)

def reset(self) -> None:
"""Reset the search engine, clearing all rules and facts."""
self._search.reset()

def add(self, text: str) -> bool:
"""Add a rule or fact to the knowledge base.

Args:
text: The rule or fact as a string.

Returns:
True if successfully added, False otherwise.
"""
return self._search.add(text)

def execute(self, callback: typing.Callable[[Rule], bool]) -> int:
"""Execute the search engine with a callback for each inferred rule.

Args:
callback: Function called for each candidate rule. Return False to continue,
True to stop.

Returns:
The number of rules processed.
"""
return self._search.execute(lambda candidate: callback(Rule(candidate.clone())))
Loading