Syntax

pynmms.syntax.Sentence dataclass

Immutable AST node for a propositional sentence.

Attributes:

Name	Type	Description
type	str	One of ATOM, NEG, CONJ, DISJ, IMPL.
name	str | None	The atom name (only when type == ATOM).
sub	Sentence | None	The sub-sentence (only when type == NEG).
left	Sentence | None	Left operand (only when type in {CONJ, DISJ, IMPL}).
right	Sentence | None	Right operand (only when type in {CONJ, DISJ, IMPL}).

Source code in src/pynmms/syntax.py

@dataclass(frozen=True, slots=True)
class Sentence:
    """Immutable AST node for a propositional sentence.

    Attributes:
        type: One of ATOM, NEG, CONJ, DISJ, IMPL.
        name: The atom name (only when type == ATOM).
        sub: The sub-sentence (only when type == NEG).
        left: Left operand (only when type in {CONJ, DISJ, IMPL}).
        right: Right operand (only when type in {CONJ, DISJ, IMPL}).
    """

    type: str
    name: str | None = None
    sub: Sentence | None = None
    left: Sentence | None = None
    right: Sentence | None = None

    def __str__(self) -> str:
        if self.type == ATOM:
            return self.name  # type: ignore[return-value]
        if self.type == NEG:
            return f"~{self.sub}"
        if self.type == CONJ:
            return f"({self.left} & {self.right})"
        if self.type == DISJ:
            return f"({self.left} | {self.right})"
        if self.type == IMPL:
            return f"({self.left} -> {self.right})"
        return f"Sentence({self.type})"  # pragma: no cover

pynmms.syntax.parse_sentence(s)

Parse a string into a propositional Sentence AST.

Examples:

>>> parse_sentence("A")
Sentence(type='atom', name='A', ...)
>>> parse_sentence("A -> B")
Sentence(type='impl', ..., left=Sentence(type='atom', name='A', ...),
         right=Sentence(type='atom', name='B', ...))

Raises:

Type	Description
ValueError	on empty input, a dangling connective, or a malformed atom.

Source code in src/pynmms/syntax.py

def parse_sentence(s: str) -> Sentence:
    """Parse a string into a propositional Sentence AST.

    Examples:
        >>> parse_sentence("A")
        Sentence(type='atom', name='A', ...)
        >>> parse_sentence("A -> B")
        Sentence(type='impl', ..., left=Sentence(type='atom', name='A', ...),
                 right=Sentence(type='atom', name='B', ...))

    Raises:
        ValueError: on empty input, a dangling connective, or a malformed atom.
    """
    s = s.strip()
    if not s:
        raise ValueError("Cannot parse empty sentence")

    # Strip outer parens if they wrap the entire expression
    if is_fully_wrapped(s):
        return parse_sentence(s[1:-1])

    # --- Binary connectives at depth 0, lowest precedence first ---

    # Implication (right-associative, lowest precedence): first match
    impl_positions = find_top_level(s, "->")
    if impl_positions:
        i = impl_positions[0]
        left_str = s[:i].strip()
        right_str = s[i + 2 :].strip()
        if not left_str or not right_str:
            raise ValueError(f"Malformed implication in: {s!r}")
        return Sentence(
            type=IMPL,
            left=parse_sentence(left_str),
            right=parse_sentence(right_str),
        )

    # Disjunction (left-associative): last match
    disj_positions = find_top_level(s, "|")
    if disj_positions:
        i = disj_positions[-1]
        left_str = s[:i].strip()
        right_str = s[i + 1 :].strip()
        if not left_str or not right_str:
            raise ValueError(f"Malformed disjunction in: {s!r}")
        return Sentence(
            type=DISJ,
            left=parse_sentence(left_str),
            right=parse_sentence(right_str),
        )

    # Conjunction (left-associative): last match
    conj_positions = find_top_level(s, "&")
    if conj_positions:
        i = conj_positions[-1]
        left_str = s[:i].strip()
        right_str = s[i + 1 :].strip()
        if not left_str or not right_str:
            raise ValueError(f"Malformed conjunction in: {s!r}")
        return Sentence(
            type=CONJ,
            left=parse_sentence(left_str),
            right=parse_sentence(right_str),
        )

    # Negation
    if s.startswith("~"):
        sub_str = s[1:].strip()
        if not sub_str:
            raise ValueError("Negation with no operand")
        return Sentence(type=NEG, sub=parse_sentence(sub_str))

    # Atom (validated)
    return Sentence(type=ATOM, name=validate_atom_name(s))

pynmms.syntax.is_atomic(s)

Return True if s parses to a bare atom (no logical connectives).

Raises ValueError if s does not parse at all (e.g. a malformed atom).

Source code in src/pynmms/syntax.py

def is_atomic(s: str) -> bool:
    """Return True if *s* parses to a bare atom (no logical connectives).

    Raises ValueError if *s* does not parse at all (e.g. a malformed atom).
    """
    return parse_sentence(s).type == ATOM

pynmms.syntax.all_atomic(sentences)

Return True if every sentence in sentences is atomic.

Source code in src/pynmms/syntax.py

def all_atomic(sentences: frozenset[str]) -> bool:
    """Return True if every sentence in *sentences* is atomic."""
    return all(is_atomic(s) for s in sentences)