CLIF Compiler

Bases: Compiler

Compiles a Theory to the Common Logic Interchange Format (CLIF).

Example:

>>> from typedlogic import Forall, Implies, PredicateDefinition, Term, Theory, Variable
>>> theory = Theory(name="friends")
>>> x = Variable("x")
>>> y = Variable("y")
>>> theory.predicate_definitions = [PredicateDefinition("FriendOf", {"x": "str", "y": "str"})]
>>> theory.add(Term("FriendOf", "Alice", "Bob"))
>>> theory.add(Forall([x, y], Implies(Term("FriendOf", x, y), Term("FriendOf", y, x))))
>>> compiler = ClifCompiler()
>>> print(compiler.compile(theory))
(cl-text friends
  (FriendOf Alice Bob)
  (forall (x y) (if (FriendOf x y) (FriendOf y x)))
)

Source code in src/typedlogic/compilers/clif_compiler.py

@dataclass
class ClifCompiler(Compiler):
    """
    Compiles a Theory to the Common Logic Interchange Format (CLIF).

    Example:
    -------
        >>> from typedlogic import Forall, Implies, PredicateDefinition, Term, Theory, Variable
        >>> theory = Theory(name="friends")
        >>> x = Variable("x")
        >>> y = Variable("y")
        >>> theory.predicate_definitions = [PredicateDefinition("FriendOf", {"x": "str", "y": "str"})]
        >>> theory.add(Term("FriendOf", "Alice", "Bob"))
        >>> theory.add(Forall([x, y], Implies(Term("FriendOf", x, y), Term("FriendOf", y, x))))
        >>> compiler = ClifCompiler()
        >>> print(compiler.compile(theory))
        (cl-text friends
          (FriendOf Alice Bob)
          (forall (x y) (if (FriendOf x y) (FriendOf y x)))
        )

    """

    default_suffix: ClassVar[str] = "clif"

    def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
        """
        Compile a Theory object into a CLIF document.

        :param theory: the theory to compile
        :param syntax: unused
        :param kwargs: unused
        :return: CLIF representation of the theory
        """
        sentences: List[Sentence] = list(theory.sentences) + list(theory.ground_terms)
        lines = [as_clif(s) for s in sentences]
        if theory.name:
            body = "\n".join(f"  {line}" for line in lines)
            if body:
                return f"(cl-text {render_name(theory.name)}\n{body}\n)"
            return f"(cl-text {render_name(theory.name)})"
        return "\n".join(lines)

    def compile_sentence(self, sentence: Sentence, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
        """
        Compile an individual sentence to CLIF.

        :param sentence: the sentence to compile
        :param syntax: unused
        :param kwargs: unused
        :return: CLIF representation of the sentence
        """
        return as_clif(sentence)

compile(theory, syntax=None, **kwargs)

Compile a Theory object into a CLIF document.

Parameters:

Name	Type	Description	Default
theory	Theory	the theory to compile	required
syntax	Optional[Union[str, ModelSyntax]]	unused	None
kwargs		unused	{}

Returns:

Type	Description
str	CLIF representation of the theory

Source code in src/typedlogic/compilers/clif_compiler.py

def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
    """
    Compile a Theory object into a CLIF document.

    :param theory: the theory to compile
    :param syntax: unused
    :param kwargs: unused
    :return: CLIF representation of the theory
    """
    sentences: List[Sentence] = list(theory.sentences) + list(theory.ground_terms)
    lines = [as_clif(s) for s in sentences]
    if theory.name:
        body = "\n".join(f"  {line}" for line in lines)
        if body:
            return f"(cl-text {render_name(theory.name)}\n{body}\n)"
        return f"(cl-text {render_name(theory.name)})"
    return "\n".join(lines)

compile_sentence(sentence, syntax=None, **kwargs)

Compile an individual sentence to CLIF.

Parameters:

Name	Type	Description	Default
sentence	Sentence	the sentence to compile	required
syntax	Optional[Union[str, ModelSyntax]]	unused	None
kwargs		unused	{}

Returns:

Type	Description
str	CLIF representation of the sentence

Source code in src/typedlogic/compilers/clif_compiler.py

def compile_sentence(self, sentence: Sentence, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
    """
    Compile an individual sentence to CLIF.

    :param sentence: the sentence to compile
    :param syntax: unused
    :param kwargs: unused
    :return: CLIF representation of the sentence
    """
    return as_clif(sentence)