Skip to content

Compilers

Framework for compiling a theory to an external format (e.g., FOL, CL, TPTP, Prolog, etc.)

ModelSyntax

Bases: str, Enum

Enum for model syntax types.

TODO: consider deprecated

Source code in src/typedlogic/compiler.py 
14
15
16
17
18
19
20
21
22
23
class ModelSyntax(str, Enum):
    """
    Enum for model syntax types.

    TODO: consider deprecated
    """

    UNKNOWN = "unknown"
    SEXPR = "sexpr"
    FUNCTIONAL = "functional"

Compiler dataclass

Bases: ABC

An engine for compiling from the internal logical model representation to an external format.

Note: one of the main use cases for compiling a theory is to generate an input for a solver. For many use cases, it's possible to just use a Solver directly, and let the system take care of compilation to an intermediate form.

You can use the registry get_compiler method to get a compiler for a particular syntax:

>>> from typedlogic.registry import get_compiler
>>> compiler = get_compiler("fol")

Next we will transpile from Python to FOL syntax. We will use a Parser object:

>>> from typedlogic.registry import get_parser
>>> parser = get_parser("python")
>>> theory = parser.parse_file("tests/theorems/animals.py")

Now we will compile the theory to FOL syntax:

>>> print(compiler.compile(theory))
Person('Fred')
Person('Jie')
Animal('corky', 'cat')
Animal('fido', 'dog')
∀[x:Thing species:Thing]. Animal(x, species) → Likes(x, 'Fred')
∀[x:Thing species:Thing]. Animal(x, 'cat') → Likes(x, 'Jie')
∀[x:Thing species:Thing]. Animal(x, 'dog') → ¬Likes('Fred', x)

Another useful syntax is TPTP, which is accepted by many theorom provers:

>>> compiler = get_compiler("tptp")
>>> print(compiler.compile(theory))
% Problem: animals
fof(axiom1, axiom, person('Fred')).
fof(axiom2, axiom, person('Jie')).
fof(axiom3, axiom, animal('corky', 'cat')).
fof(axiom4, axiom, animal('fido', 'dog')).
fof(axiom5, axiom, ! [X, Species] : (animal(X, Species) => likes(X, 'Fred'))).
fof(axiom6, axiom, ! [X, Species] : (animal(X, 'cat') => likes(X, 'Jie'))).
fof(axiom7, axiom, ! [X, Species] : (animal(X, 'dog') => ~likes('Fred', X))).

Another common syntax is Prolog syntax, and its variants. These are often used by Datalog solvers:

>>> compiler = get_compiler("prolog")
>>> print(compiler.compile(theory))
%% Predicate Definitions
% Likes(subject: str, object: str)
% Person(name: str)
% Animal(name: str, species: str)
<BLANKLINE>
%% persons
<BLANKLINE>
person('Fred').
person('Jie').
<BLANKLINE>
%% animals
<BLANKLINE>
animal('corky', 'cat').
animal('fido', 'dog').
<BLANKLINE>
%% animal_preferences
<BLANKLINE>
likes(X, 'Fred') :- animal(X, Species).
likes(X, 'Jie') :- animal(X, 'cat').
<BLANKLINE>
Source code in src/typedlogic/compiler.py 
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
@dataclass
class Compiler(ABC):
    """
    An engine for compiling from the internal logical model representation to an external format.

    Note: one of the main use cases for compiling a theory is to generate an input for a solver.
    For many use cases, it's possible to just use a Solver directly, and let the system
    take care of compilation to an intermediate form.

    You can use the registry `get_compiler` method to get a compiler for a particular syntax:

        >>> from typedlogic.registry import get_compiler
        >>> compiler = get_compiler("fol")

    Next we will transpile from Python to FOL syntax. We will use a `Parser` object:

        >>> from typedlogic.registry import get_parser
        >>> parser = get_parser("python")
        >>> theory = parser.parse_file("tests/theorems/animals.py")

    Now we will compile the theory to FOL syntax:

        >>> print(compiler.compile(theory))
        Person('Fred')
        Person('Jie')
        Animal('corky', 'cat')
        Animal('fido', 'dog')
        ∀[x:Thing species:Thing]. Animal(x, species) → Likes(x, 'Fred')
        ∀[x:Thing species:Thing]. Animal(x, 'cat') → Likes(x, 'Jie')
        ∀[x:Thing species:Thing]. Animal(x, 'dog') → ¬Likes('Fred', x)

    Another useful syntax is TPTP, which is accepted by many theorom provers:

        >>> compiler = get_compiler("tptp")
        >>> print(compiler.compile(theory))
        % Problem: animals
        fof(axiom1, axiom, person('Fred')).
        fof(axiom2, axiom, person('Jie')).
        fof(axiom3, axiom, animal('corky', 'cat')).
        fof(axiom4, axiom, animal('fido', 'dog')).
        fof(axiom5, axiom, ! [X, Species] : (animal(X, Species) => likes(X, 'Fred'))).
        fof(axiom6, axiom, ! [X, Species] : (animal(X, 'cat') => likes(X, 'Jie'))).
        fof(axiom7, axiom, ! [X, Species] : (animal(X, 'dog') => ~likes('Fred', X))).

    Another common syntax is Prolog syntax, and its variants. These are often used by Datalog solvers:

        >>> compiler = get_compiler("prolog")
        >>> print(compiler.compile(theory))
        %% Predicate Definitions
        % Likes(subject: str, object: str)
        % Person(name: str)
        % Animal(name: str, species: str)
        <BLANKLINE>
        %% persons
        <BLANKLINE>
        person('Fred').
        person('Jie').
        <BLANKLINE>
        %% animals
        <BLANKLINE>
        animal('corky', 'cat').
        animal('fido', 'dog').
        <BLANKLINE>
        %% animal_preferences
        <BLANKLINE>
        likes(X, 'Fred') :- animal(X, Species).
        likes(X, 'Jie') :- animal(X, 'cat').
        <BLANKLINE>


    """

    default_suffix: ClassVar[str] = "txt"
    parser_class: ClassVar[Optional[Type[Parser]]] = None
    strict: Optional[bool] = None

    @abstractmethod
    def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
        """
        Compile a theory into an external representation.

        :param theory:
        :param syntax:
        :param kwargs:
        :return: string representation of the compiled artefact
        """
        pass

    def compile_to_target(
        self,
        theory: Theory,
        target: Union[str, Path, TextIO],
        syntax: Optional[Union[str, ModelSyntax]] = None,
        **kwargs,
    ):
        """
        Compile a theory to a file or stream.

        :param theory:
        :param target:
        :param syntax:
        :param kwargs:
        :return:
        """
        if isinstance(target, str):
            target = Path(target)
        if isinstance(target, Path):
            with target.open("w") as f:
                f.write(self.compile(theory, syntax=syntax, **kwargs))
        else:
            target.write(self.compile(theory, syntax=syntax, **kwargs))

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

        :param sentence:
        :param syntax:
        :param kwargs:
        :return:
        """
        theory = Theory()
        theory.add(sentence)
        return self.compile(theory, syntax=syntax, **kwargs)

    @property
    def suffix(self) -> str:
        """
        Get the suffix for the compiled output.

        :return:
        """
        return self.default_suffix

    def _add_untranslatable(self, sentence: Sentence):
        pass

suffix: str property

Get the suffix for the compiled output.

Returns:

Type Description
str

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

Compile a theory into an external representation.

Parameters:

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

Returns:

Type Description
str

string representation of the compiled artefact
Source code in src/typedlogic/compiler.py 
102
103
104
105
106
107
108
109
110
111
112
@abstractmethod
def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
    """
    Compile a theory into an external representation.

    :param theory:
    :param syntax:
    :param kwargs:
    :return: string representation of the compiled artefact
    """
    pass

compile_to_target(theory, target, syntax=None, **kwargs)

Compile a theory to a file or stream.

Parameters:

Name Type Description Default
theory Theory
required
target Union[str, Path, TextIO]
required
syntax Optional[Union[str, ModelSyntax]]
None
kwargs
{}

Returns:

Type Description
Source code in src/typedlogic/compiler.py 
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
def compile_to_target(
    self,
    theory: Theory,
    target: Union[str, Path, TextIO],
    syntax: Optional[Union[str, ModelSyntax]] = None,
    **kwargs,
):
    """
    Compile a theory to a file or stream.

    :param theory:
    :param target:
    :param syntax:
    :param kwargs:
    :return:
    """
    if isinstance(target, str):
        target = Path(target)
    if isinstance(target, Path):
        with target.open("w") as f:
            f.write(self.compile(theory, syntax=syntax, **kwargs))
    else:
        target.write(self.compile(theory, syntax=syntax, **kwargs))

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

Compiles an individual sentence

Parameters:

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

Returns:

Type Description
str
Source code in src/typedlogic/compiler.py 
138
139
140
141
142
143
144
145
146
147
148
149
def compile_sentence(self, sentence: Sentence, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
    """
    Compiles an individual sentence

    :param sentence:
    :param syntax:
    :param kwargs:
    :return:
    """
    theory = Theory()
    theory.add(sentence)
    return self.compile(theory, syntax=syntax, **kwargs)