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."""
        text = self._read_source(source)
        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."""
        try:
            self.parse(source, **kwargs)
        except LarkError as e:
            yield ValidationMessage(message=str(e))

    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 statement.comments:
            sentence.add_annotation("comment", "\n".join(statement.comments))
        theory.add(sentence)

    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, 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 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.

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."""
    text = self._read_source(source)
    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

validate_iter(source, **kwargs)

Validate source syntax.

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."""
    try:
        self.parse(source, **kwargs)
    except LarkError as e:
        yield ValidationMessage(message=str(e))

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 parse(self, source: Union[Path, str, TextIO], **kwargs: Any) -> Theory:
        """Parse fenced TLog code blocks from Markdown into a theory."""
        text = self._read_source(source)
        return super().parse(self._extract_tlog_blocks(text), **kwargs)

    def _extract_tlog_blocks(self, text: str) -> str:
        blocks: list[str] = []
        block_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]
                language = stripped[3:].strip().split(maxsplit=1)[0].lower()
                collecting = language in self.code_block_languages
                in_block = True
                block_lines = []
                continue
            if in_block and stripped.startswith(fence):
                if collecting:
                    blocks.append("\n".join(block_lines))
                in_block = False
                collecting = False
                fence = ""
                block_lines = []
                continue
            if collecting:
                block_lines.append(line)

        if in_block and collecting:
            blocks.append("\n".join(block_lines))

        return "\n\n".join(blocks)

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

parse(source, **kwargs)

Parse fenced TLog code blocks from Markdown into a theory.

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

def parse(self, source: Union[Path, str, TextIO], **kwargs: Any) -> Theory:
    """Parse fenced TLog code blocks from Markdown into a theory."""
    text = self._read_source(source)
    return super().parse(self._extract_tlog_blocks(text), **kwargs)

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 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).

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

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.