TLog Parser

TLog is a compact text syntax for authoring TypedLogic theories without using Python. It is still just another TypedLogic parser: the same convert, dump, and solve commands work with it.

Bases: Parser

Parse ergonomic TypedLogic rules into the core datamodel.

Source code in src/typedlogic/parsers/tlog_parser.py

class TLogParser(Parser):
    """Parse ergonomic TypedLogic rules into the core datamodel."""

    default_suffix = "tlog"

    def __init__(self, implicit_universal: bool = True, **kwargs: Any):
        """
        Create a parser.

        :param implicit_universal: Wrap unquantified rules containing variables in `Forall`.
        :param kwargs: Forwarded to the base parser.
        """
        super().__init__(**kwargs)
        self.implicit_universal = implicit_universal
        self._parser = Lark(GRAMMAR, parser="lalr", propagate_positions=True, maybe_placeholders=False)

    def parse(self, source: Union[Path, str, TextIO], **kwargs: Any) -> Theory:
        """
        Parse a TLog source into a theory.

        Parsing is permissive: an *undeclared* predicate may be used at any arity, mirroring
        Prolog where ``person/1`` and ``person/2`` are distinct relations. If ``auto_validate``
        is set, a *declared* predicate used at an arity no declaration matches raises an error
        (see :meth:`validate_iter`).
        """
        theory = self._build_theory(self._prepare_text(source))
        if self.auto_validate:
            errors = [m for m in self._arity_messages(theory) if m.level == "error"]
            if errors:
                raise ValueError("Validation errors: " + "; ".join(m.message for m in errors))
        return theory

    def _prepare_text(self, source: Union[Path, str, TextIO]) -> str:
        """Return the TLog text to parse from a source. Subclasses may preprocess here."""
        return self._read_source(source)

    def _build_theory(self, text: str) -> Theory:
        """Parse already-prepared TLog text into a theory, without validation side effects."""
        tree = self._parser.parse(text)
        statement_nodes = _TreeToNodes().transform(tree)
        theory = Theory()
        for statement in statement_nodes.children:
            self._add_statement(theory, statement)
        return theory

    def validate_iter(self, source: Union[Path, str, TextIO], **kwargs: Any) -> Iterable[ValidationMessage]:
        """
        Validate source syntax and predicate-arity usage.

        Reports a syntax error for unparsable input, and an error for any *declared* predicate
        used at an arity that no declaration provides. Undeclared predicates are not checked, so
        the same name may still be used at multiple arities when no ``pred`` declaration exists.
        """
        try:
            theory = self._build_theory(self._prepare_text(source))
        except (LarkError, ValueError) as e:
            line = getattr(e, "line", None)
            column = getattr(e, "column", None)
            yield ValidationMessage(message=_LARK_LOCATION_RE.sub(".", str(e), count=1), line=line, column=column)
            return
        yield from self._arity_messages(theory)

    def _arity_messages(self, theory: Theory) -> Iterable[ValidationMessage]:
        """Yield an error for each declared predicate used at an undeclared arity."""
        declared: dict[str, set[int]] = {}
        for pd in theory.predicate_definitions:
            declared.setdefault(pd.predicate, set()).add(len(pd.arguments))
        if not declared:
            return
        reported: set[tuple[str, int]] = set()
        for sentence in self._validation_sentences(theory):
            for name, arity in self._predicate_usages(sentence):
                if name not in declared or arity in declared[name] or (name, arity) in reported:
                    continue
                reported.add((name, arity))
                expected = ", ".join(f"{name}/{a}" for a in sorted(declared[name]))
                yield ValidationMessage(
                    message=(
                        f"Predicate '{name}' used with arity {arity}, but declared as {expected}. "
                        f"Add 'pred {name}/{arity}.' if the {arity}-ary use is intentional."
                    ),
                    level="error",
                )

    def _validation_sentences(self, theory: Theory) -> Iterable[Sentence]:
        """Yield every sentence represented by the source, including metadata groups."""
        for group in theory.sentence_groups:
            yield from group.sentences or []

    def _predicate_usages(self, node: Any) -> Iterable[tuple[str, int]]:
        """Yield ``(predicate_name, arity)`` for every non-builtin atom in a sentence tree."""
        if isinstance(node, Term):
            predicate = node.predicate
            if isinstance(predicate, str) and predicate not in NUMERIC_BUILTINS:
                yield (predicate, len(node.values))
            for value in node.values:
                yield from self._predicate_usages(value)
            return
        if isinstance(node, (Forall, Exists)):
            yield from self._predicate_usages(node.sentence)
            return
        operands = getattr(node, "operands", None)
        if operands is not None:
            for operand in operands:
                yield from self._predicate_usages(operand)

    def _read_source(self, source: Union[Path, str, TextIO]) -> str:
        if isinstance(source, Path):
            return source.read_text(encoding="utf-8")
        if hasattr(source, "read"):
            return source.read()
        return str(source)

    def _add_statement(self, theory: Theory, statement: StatementNode) -> None:
        body = statement.body
        if isinstance(body, TypeDecl):
            theory.type_definitions[body.name] = body.base
            return
        if isinstance(body, PredicateArityDecl):
            theory.predicate_definitions.append(
                PredicateDefinition(body.name, {f"arg{i}": "str" for i in range(body.arity)})
            )
            return
        if isinstance(body, PredicateSignatureDecl):
            theory.predicate_definitions.append(PredicateDefinition(body.name, dict(body.arguments)))
            return

        sentence = self._lower_statement(body)
        if self._add_meta_statement(theory, sentence, statement.comments):
            return
        if statement.comments:
            sentence.add_annotation("comment", "\n".join(statement.comments))
        theory.add(sentence)

    def _add_meta_statement(self, theory: Theory, sentence: Sentence, comments: tuple[str, ...]) -> bool:
        """Add top-level quoted meta statements as sentence groups."""
        if not isinstance(sentence, Term):
            return False
        if sentence.predicate == "lemma":
            name, quoted = self._named_quoted_sentence(sentence, "lemma")
            theory.sentence_groups.append(
                SentenceGroup(
                    name=name,
                    group_type=SentenceGroupType.LEMMA,
                    docstring="\n".join(comments) or None,
                    sentences=[quoted],
                )
            )
            return True
        if sentence.predicate == "test_case":
            name = str(sentence.values[0]) if sentence.values else "test_case"
            theory.sentence_groups.append(
                SentenceGroup(
                    name=name,
                    group_type=SentenceGroupType.TEST,
                    docstring="\n".join(comments) or None,
                    sentences=[sentence],
                )
            )
            return True
        return False

    def _named_quoted_sentence(self, sentence: Term, predicate: str) -> tuple[str, Sentence]:
        """Return the name and quoted sentence from a meta term."""
        if len(sentence.values) != 2:
            raise LarkError(f"{predicate} expects a name and that(sentence): {sentence}")
        name, quoted = sentence.values
        inner = self._quoted_sentence_value(quoted)
        return str(name), inner

    def _quoted_sentence_value(self, value: Any) -> Sentence:
        """Return the sentence wrapped by a that(...) term."""
        if not isinstance(value, Term) or value.predicate != "that" or len(value.values) != 1:
            raise LarkError(f"Expected that(sentence), got {value}")
        quoted = value.values[0]
        if not isinstance(quoted, Sentence):
            raise LarkError(f"Expected quoted sentence, got {quoted}")
        return quoted

    def _lower_statement(self, node: Any) -> Sentence:
        explicit_vars = self._explicit_vars(node)
        rule_like = bool(explicit_vars) or self._is_rule_like(node)
        sentence = self._lower(node, explicit_vars, bare_names_as_variables=rule_like)
        if explicit_vars:
            return sentence
        variables = self._sentence_variables(sentence)
        if self.implicit_universal and variables and rule_like:
            return Forall(variables, sentence)
        return sentence

    def _lower(self, node: Any, bound_vars: dict[str, Variable], bare_names_as_variables: bool) -> Any:
        if isinstance(node, QuantifierNode):
            local_vars = {**bound_vars, **{v.name: v for v in node.variables}}
            sentence = self._lower(node.sentence, local_vars, bare_names_as_variables=False)
            if node.quantifier == "forall":
                return Forall(list(node.variables), sentence)
            return Exists(list(node.variables), sentence)
        if isinstance(node, ConstraintNode):
            return Implies(self._lower(node.body, bound_vars, bare_names_as_variables), Or())
        if isinstance(node, UnaryNode):
            operand = self._lower(node.operand, bound_vars, bare_names_as_variables)
            if node.operator == "naf":
                return NegationAsFailure(operand)
            return Not(operand)
        if isinstance(node, ThatNode):
            return Term("that", self._lower_statement(node.sentence))
        if isinstance(node, BinaryNode):
            left = self._lower(node.left, bound_vars, bare_names_as_variables)
            right = self._lower(node.right, bound_vars, bare_names_as_variables)
            if node.operator == "and":
                return And(left, right)
            if node.operator == "or":
                return Or(left, right)
            if node.operator == "implies":
                return Implies(left, right)
            if node.operator == "iff":
                return Iff(left, right)
            raise ValueError(f"Unknown operator: {node.operator}")
        if isinstance(node, AtomNode):
            predicate: Union[str, Variable] = node.predicate.name
            if node.predicate.variable:
                predicate = bound_vars.get(node.predicate.name, Variable(node.predicate.name))
            args = [self._lower(arg, bound_vars, bare_names_as_variables) for arg in node.arguments]
            return Term(predicate, *args)
        if isinstance(node, Term):
            args = [self._lower(arg, bound_vars, bare_names_as_variables) for arg in node.values]
            return Term(node.predicate, *args)
        if isinstance(node, NameRef):
            if node.variable:
                return bound_vars.get(node.name, Variable(node.name))
            if node.name in bound_vars:
                return bound_vars[node.name]
            if bare_names_as_variables:
                return Variable(node.name)
            return node.name
        if isinstance(node, bool):
            return And() if node else Or()
        return node

    def _explicit_vars(self, node: Any) -> dict[str, Variable]:
        if isinstance(node, QuantifierNode):
            return {v.name: v for v in node.variables}
        return {}

    def _is_rule_like(self, node: Any) -> bool:
        if isinstance(node, (ConstraintNode, QuantifierNode)):
            return True
        if isinstance(node, BinaryNode):
            if node.operator in {"implies", "iff"}:
                return True
            return self._is_rule_like(node.left) or self._is_rule_like(node.right)
        if isinstance(node, UnaryNode):
            return self._is_rule_like(node.operand)
        return False

    def _sentence_variables(self, sentence: Any) -> list[Variable]:
        variables: list[Variable] = []
        seen: set[str] = set()

        def visit(value: Any) -> None:
            if isinstance(value, Variable):
                if value.name not in seen:
                    seen.add(value.name)
                    variables.append(value)
                return
            if isinstance(value, Term):
                if value.predicate == "that":
                    return
                if isinstance(value.predicate, Variable):
                    visit(value.predicate)
                for arg in value.values:
                    visit(arg)
                return
            if isinstance(value, (Forall, Exists)):
                for var in value.variables:
                    seen.add(var.name)
                visit(value.sentence)
                return
            if isinstance(value, (And, Or, Not, NegationAsFailure, Implies, Iff)):
                for operand in value.operands:
                    visit(operand)

        visit(sentence)
        return variables

__init__(implicit_universal=True, **kwargs)

Create a parser.

Parameters:

Name	Type	Description	Default
implicit_universal	bool	Wrap unquantified rules containing variables in Forall.	True
kwargs	Any	Forwarded to the base parser.	{}

Source code in src/typedlogic/parsers/tlog_parser.py

def __init__(self, implicit_universal: bool = True, **kwargs: Any):
    """
    Create a parser.

    :param implicit_universal: Wrap unquantified rules containing variables in `Forall`.
    :param kwargs: Forwarded to the base parser.
    """
    super().__init__(**kwargs)
    self.implicit_universal = implicit_universal
    self._parser = Lark(GRAMMAR, parser="lalr", propagate_positions=True, maybe_placeholders=False)

parse(source, **kwargs)

Parse a TLog source into a theory.

Parsing is permissive: an undeclared predicate may be used at any arity, mirroring Prolog where person/1 and person/2 are distinct relations. If auto_validate is set, a declared predicate used at an arity no declaration matches raises an error (see :meth:validate_iter).

Source code in src/typedlogic/parsers/tlog_parser.py

def parse(self, source: Union[Path, str, TextIO], **kwargs: Any) -> Theory:
    """
    Parse a TLog source into a theory.

    Parsing is permissive: an *undeclared* predicate may be used at any arity, mirroring
    Prolog where ``person/1`` and ``person/2`` are distinct relations. If ``auto_validate``
    is set, a *declared* predicate used at an arity no declaration matches raises an error
    (see :meth:`validate_iter`).
    """
    theory = self._build_theory(self._prepare_text(source))
    if self.auto_validate:
        errors = [m for m in self._arity_messages(theory) if m.level == "error"]
        if errors:
            raise ValueError("Validation errors: " + "; ".join(m.message for m in errors))
    return theory

validate_iter(source, **kwargs)

Validate source syntax and predicate-arity usage.

Reports a syntax error for unparsable input, and an error for any declared predicate used at an arity that no declaration provides. Undeclared predicates are not checked, so the same name may still be used at multiple arities when no pred declaration exists.

Source code in src/typedlogic/parsers/tlog_parser.py

def validate_iter(self, source: Union[Path, str, TextIO], **kwargs: Any) -> Iterable[ValidationMessage]:
    """
    Validate source syntax and predicate-arity usage.

    Reports a syntax error for unparsable input, and an error for any *declared* predicate
    used at an arity that no declaration provides. Undeclared predicates are not checked, so
    the same name may still be used at multiple arities when no ``pred`` declaration exists.
    """
    try:
        theory = self._build_theory(self._prepare_text(source))
    except (LarkError, ValueError) as e:
        line = getattr(e, "line", None)
        column = getattr(e, "column", None)
        yield ValidationMessage(message=_LARK_LOCATION_RE.sub(".", str(e), count=1), line=line, column=column)
        return
    yield from self._arity_messages(theory)

Bases: TLogParser

Parse TLog blocks embedded in Markdown prose.

Source code in src/typedlogic/parsers/tlog_parser.py

class TLogMarkdownParser(TLogParser):
    """Parse TLog blocks embedded in Markdown prose."""

    default_suffix = "tlog.md"
    code_block_languages = frozenset({"tlog", "typedlogic", "logic"})

    def _prepare_text(self, source: Union[Path, str, TextIO]) -> str:
        """Extract fenced TLog code blocks from Markdown before parsing/validation."""
        return self._extract_tlog_blocks(self._read_source(source))

    def _extract_tlog_blocks(self, text: str) -> str:
        lines: list[str] = []
        in_block = False
        collecting = False
        fence = ""

        for line in text.splitlines():
            stripped = line.strip()
            if not in_block and self._starts_fence(stripped):
                fence = stripped[:3]
                info = stripped[3:].strip().split(maxsplit=1)
                language = info[0].lower() if info else ""
                collecting = language in self.code_block_languages
                in_block = True
                lines.append("")
                continue
            if in_block and stripped.startswith(fence):
                in_block = False
                collecting = False
                fence = ""
                lines.append("")
                continue
            if collecting:
                lines.append(line)
                continue
            lines.append("")

        return "\n".join(lines)

    def _starts_fence(self, stripped: str) -> bool:
        return stripped.startswith("```") or stripped.startswith("~~~")

Syntax

type PersonID: str.

pred parent(parent: PersonID, child: PersonID).
pred ancestor(ancestor: PersonID, descendant: PersonID).

parent("Alice", "Bob").
parent("Bob", "Charlie").

/// Direct parent links are ancestor links.
ancestor(x, y) :- parent(x, y).

/// Ancestor links are transitive.
ancestor(x, z) :- ancestor(x, y), ancestor(y, z).

Types are optional. Untyped targets can ignore them; typed targets such as Souffle can use them.

Predicate Arity Validation

Parsing is permissive: an undeclared predicate may be used at any arity, just as Prolog treats person/1 and person/2 as distinct relations. Declaring a predicate signals intent, so once a name is declared with pred, using it at an arity that no declaration matches is reported as a validation error. This catches a common mistake — writing a constraint against the wrong arity, which silently refers to a different (empty) relation instead of the declared facts:

pred foo(x: int, y: int).
foo(1, 1).
foo(1, 2).

/// BUG: foo/1 here is a different relation from the declared foo/2, so this
/// constraint is vacuously true and never contradicts the facts above.
all i, j | foo(i), foo(j) -> i = j.

Validation reports an error for the foo/1 use. The intended functional-dependency constraint compares the second column for a shared first column:

all x, y1, y2 | foo(x, y1), foo(x, y2) -> y1 = y2.

If a name genuinely needs multiple arities, declare each one (pred foo/1. and pred foo(x: int, y: int).). Errors surface through parser.validate(...), the CLI (e.g. convert --validate-types), or eagerly at parse time when the parser is constructed with auto_validate=True.

Predicate and variable names are case-preserving. Variables are not inferred from capitalization. In a rule or explicit quantifier, bare names are variables:

ancestor(x, Y) :- parent(x, z), ancestor(z, Y).

In facts, bare names are constants:

parent(Alice, Bob).

Use quoted strings when a constant appears in a rule body or head:

favorite_child(x) :- parent("Alice", x).

Quantifiers

Explicit universal and existential quantifiers are available:

all x, y | parent(x, y) -> ancestor(x, y).
exists witness | observed(witness).

The classic symbols are accepted aliases:

∀ x, y | parent(x, y) -> ancestor(x, y).
∃ witness | observed(witness).

If you need to disambiguate a variable without an explicit quantifier, use ?:

likes(?person, "tea") -> happy(?person).

Quoted Meta Statements

Use that(...) to quote a sentence as data. Quoted sentences are not asserted unless a runner explicitly interprets them.

Lemmas are named proof obligations:

lemma(
  "grandparent_implies_ancestor",
  that(all x, y, z | parent(x, y) & parent(y, z) -> ancestor(x, z))
).

Test cases can carry quoted fixtures and expectations without sending them to the solver as ordinary facts:

test_case(
  "socrates_mortality",
  given(that(human("socrates"))),
  expect(that(satisfiable() & mortal("socrates") & not philosopher("socrates")))
).

solve ignores lemmas and test cases by default. Use test when you want a one-stop validation command for both test cases and proof obligations; use prove when you only want goals and lemmas:

typedlogic test theory.tlog --solver clingo
typedlogic prove theory.tlog --solver z3 --target lemmas

The test runner treats given(that(S)) as a temporary assertion for that test case. expect(that(E)) checks the expected sentence. In expectations, satisfiable() is a built-in check for fixture satisfiability, conjunction means all expectations must hold, and not P means P is not entailed. After running test cases, test also proves matching goals and lemmas unless --no-proofs is used.

HiLog-Style Predicate Variables

Use @name(...) to put a variable in predicate position:

all slot, i, v | @slot(i, v) -> has_slot_value(i, slot).

This is useful for schema or macro-expansion layers. Backends that require fixed first-order predicate names may reject such sentences until they are expanded.

Literate Markdown

Markdown files ending in .tlog.md are parsed by TLogMarkdownParser. Prose is ignored and fenced tlog, typedlogic, or logic blocks are parsed in order:

# Family rules

Only this fenced block is parsed:

```tlog
pred parent(parent: str, child: str).
pred ancestor(ancestor: str, descendant: str).
ancestor(x, y) :- parent(x, y).
```

CLI

The CLI auto-detects .tlog and .tlog.md files. Use -f tlog or -f tlogmarkdown only when the suffix does not identify the format.

Convert TLog to another format:

typedlogic convert docs/examples/tlog/ancestor.tlog -t prolog
typedlogic convert docs/examples/tlog/ancestor.tlog -t yaml
typedlogic convert docs/examples/tlog/ancestor.tlog -t souffle

Convert any parser-supported input to TLog:

typedlogic convert docs/examples/tlog/ancestor.tlog -t tlog

Use dump when combining multiple input files or when you want pure auto-detection:

typedlogic dump docs/examples/tlog/literate-rules.tlog.md -t prolog

Run inference with any installed solver:

typedlogic solve docs/examples/tlog/ancestor.tlog --solver clingo

Lemmas and test cases are metadata, so solve does not run or assert them. Run validation explicitly with test:

typedlogic test docs/examples/tlog/mortality.tlog --solver clingo
typedlogic test docs/examples/tlog/mortality.tlog --solver clingo --test socrates_mortality

test also proves goals and lemmas by default. Use prove for proof-only runs:

typedlogic prove docs/examples/tlog/mortality.tlog --solver z3
typedlogic prove docs/examples/tlog/mortality.tlog --solver z3 --target lemmas
typedlogic prove docs/examples/tlog/mortality.tlog --solver z3 --name socrates_is_mortal

Show only selected materialized predicates:

typedlogic solve docs/examples/tlog/ancestor.tlog \
  --solver clingo \
  --show ancestor \
  --max-models 1

Show multiple answer sets:

typedlogic solve docs/examples/tlog/worlds.tlog \
  --solver clingo \
  --show selected \
  --max-models 2

The --show and --max-models options are generic solve options, not TLog-specific commands.

Dump the generated solver program before solving:

typedlogic solve docs/examples/tlog/ancestor.tlog \
  --solver clingo \
  --dump-program