Formula AST API

Status: Generated from current Python docstrings and type hints.

Predicate-logic primitive types, terms, formula nodes, connectives, symbols, and quantifiers.

gaia.engine.lang.formula

Gaia Lang Formula AST — typed term, predicate, connective, quantifier nodes.

Iff dataclass

Iff(left: Any, right: Any)

Logical equivalence between two Formula operands.

Implies dataclass

Implies(antecedent: Any, consequent: Any)

Logical implication from antecedent Formula to consequent Formula.

Land dataclass

Land(operands: tuple[Any, ...])

Logical conjunction over two or more Formula operands.

Lnot dataclass

Lnot(operand: Any)

Logical negation of a Formula operand.

Lor dataclass

Lor(operands: tuple[Any, ...])

Logical disjunction over two or more Formula operands.

ClaimAtom dataclass

ClaimAtom(claim: Claim)

A reference to another Claim's truth — the bridge from formula land to claim graph.

Equals dataclass

Equals(left: Any, right: Any)

Term equality formula.

Formula

Bases: Protocol

Marker protocol — a truth-valued AST node.

Greater dataclass

Greater(left: Any, right: Any)

Greater-than relation over Term operands.

GreaterEqual dataclass

GreaterEqual(left: Any, right: Any)

Greater-than-or-equal relation over Term operands.

Less dataclass

Less(left: Any, right: Any)

Less-than relation over Term operands.

LessEqual dataclass

LessEqual(left: Any, right: Any)

Less-than-or-equal relation over Term operands.

NotEquals dataclass

NotEquals(left: Any, right: Any)

Term inequality formula.

UserPredicate dataclass

UserPredicate(symbol: PredicateSymbol, args: tuple[Any, ...])

Application of a user-declared PredicateSymbol to typed Term arguments.

PrimitiveType

PrimitiveType(name: str, accept: Callable[[object], bool])

A built-in typed sort. Construction is sealed once the module finishes loading.

Create a primitive type token before the module is sealed.

Source code in gaia/engine/lang/formula/primitives.py

def __init__(self, name: str, accept: Callable[[object], bool]) -> None:
    """Create a primitive type token before the module is sealed."""
    if _SEALED:
        raise TypeError(
            "PrimitiveType is sealed. Use the four built-ins: Nat, Real, Probability, Bool."
        )
    self.name = name
    self._accept = accept

accepts

accepts(value: object) -> bool

Return whether value belongs to this primitive type.

Source code in gaia/engine/lang/formula/primitives.py

def accepts(self, value: object) -> bool:
    """Return whether ``value`` belongs to this primitive type."""
    return self._accept(value)

FunctionSymbol dataclass

FunctionSymbol(name: str, arg_domains: tuple[PrimitiveType | Domain, ...], result_domain: PrimitiveType | Domain)

Declaration of a user function symbol like E: Particle → Real.

PredicateSymbol dataclass

PredicateSymbol(name: str, arg_domains: tuple[PrimitiveType | Domain, ...])

Declaration of a user predicate symbol like Stable: Particle → Bool.

ArithOp dataclass

ArithOp(op: str, left: Any, right: Any)

An arithmetic operation between two Terms.

Constant dataclass

Constant(value: Any, primitive: PrimitiveType)

A primitive literal value, validated against its declared PrimitiveType.

FunctionApp dataclass

FunctionApp(symbol: FunctionSymbol, args: tuple[Any, ...])

Application of a FunctionSymbol to a tuple of Term arguments.

Term

Bases: Protocol

Marker protocol. A Term is a value-bearing expression node.

is_formula

is_formula(obj: object) -> bool

Return whether an object is explicitly tagged as a Formula node.

Source code in gaia/engine/lang/formula/predicate.py

def is_formula(obj: object) -> bool:
    """Return whether an object is explicitly tagged as a Formula node."""
    return getattr(obj, "__gaia_formula__", False) is True

is_term

is_term(obj: object) -> bool

Strict check — only objects explicitly tagged as terms qualify.

Source code in gaia/engine/lang/formula/term.py

def is_term(obj: object) -> bool:
    """Strict check — only objects explicitly tagged as terms qualify."""
    return getattr(obj, "__gaia_term__", False) is True