Skip to content

Python Parser

Bases: Parser

A parser for Python modules that contain axioms.

Example:

>>> parser = PythonParser()
>>> theory = parser.parse(Path("tests/theorems/mortals.py"))
>>> assert isinstance(theory, Theory)
>>> theory.name
'mortals'
>>> [pd.predicate for pd in theory.predicate_definitions]
['Person', 'Mortal', 'AncestorOf']
>>> for s in sorted(theory.sentences):
...     print(s)
((AncestorOf(p1, p2)) & (AncestorOf(p2, p3)) -> AncestorOf(p1, p3))
∀x: TreeNodeType, y: TreeNodeType : ~(AncestorOf(?x, ?y)) & (AncestorOf(?y, ?x))
∀x: TreeNodeType, y: TreeNodeType, z: TreeNodeType : ((AncestorOf(?x, ?z)) & (AncestorOf(?z, ?y)) -> AncestorOf(?x, ?y))
∀x: NameType : (Person(?x) -> Mortal(?x))

Inheritance:

>>> theory = parser.parse(Path("tests/theorems/class_inheritance.py"))
>>> theory.name
'class_inheritance'
>>> [(pd.predicate, pd.parents) for pd in theory.predicate_definitions]
[('Thing', []), ('Place', ['Thing']), ('Person', ['Thing'])]
>>> from typedlogic.transformations import implies_from_parents
>>> # TODO - consider making this default
>>> theory = implies_from_parents(theory)
>>> for s in sorted(theory.sentences):
...     print(s)
∀name: str, age: int : (Person(?name, ?age) -> Thing(?name))
∀name: str : (Place(?name) -> Thing(?name))
Source code in src/typedlogic/parsers/pyparser/python_parser.py 
 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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
class PythonParser(Parser):
    """
    A parser for Python modules that contain axioms.

    Example:

        >>> parser = PythonParser()
        >>> theory = parser.parse(Path("tests/theorems/mortals.py"))
        >>> assert isinstance(theory, Theory)
        >>> theory.name
        'mortals'
        >>> [pd.predicate for pd in theory.predicate_definitions]
        ['Person', 'Mortal', 'AncestorOf']
        >>> for s in sorted(theory.sentences):
        ...     print(s)
        ((AncestorOf(p1, p2)) & (AncestorOf(p2, p3)) -> AncestorOf(p1, p3))
        ∀x: TreeNodeType, y: TreeNodeType : ~(AncestorOf(?x, ?y)) & (AncestorOf(?y, ?x))
        ∀x: TreeNodeType, y: TreeNodeType, z: TreeNodeType : ((AncestorOf(?x, ?z)) & (AncestorOf(?z, ?y)) -> AncestorOf(?x, ?y))
        ∀x: NameType : (Person(?x) -> Mortal(?x))

    Inheritance:

        >>> theory = parser.parse(Path("tests/theorems/class_inheritance.py"))
        >>> theory.name
        'class_inheritance'
        >>> [(pd.predicate, pd.parents) for pd in theory.predicate_definitions]
        [('Thing', []), ('Place', ['Thing']), ('Person', ['Thing'])]
        >>> from typedlogic.transformations import implies_from_parents
        >>> # TODO - consider making this default
        >>> theory = implies_from_parents(theory)
        >>> for s in sorted(theory.sentences):
        ...     print(s)
        ∀name: str, age: int : (Person(?name, ?age) -> Thing(?name))
        ∀name: str : (Place(?name) -> Thing(?name))

    """

    def transform(self, source: ModuleType, **kwargs) -> Theory:
        """
        Transform a Python module into a Theory

        :param source:
        :param kwargs:
        :return:
        """
        return translate_module_to_theory(source)

    def parse(self, source: Union[Path, str, TextIO, ModuleType], file_name: Optional[str] = None, **kwargs) -> Theory:
        """
        Parse a Python module or source code into a Theory.

        :param source:
        :param file_name:
        :param kwargs:
        :return:
        """
        if isinstance(source, ModuleType):
            return translate_module_to_theory(source)
        if self.auto_validate:
            errs = self.validate(source)
            if errs:
                raise ValueError(f"Validation errors: {errs}")
        if isinstance(source, Path):
            with source.open() as f:
                return self.parse(f, file_name=str(source), **kwargs)
        if isinstance(source, str):
            module = compile_python(source, name=None, package_path=file_name)
            sgs = get_module_sentence_groups(source)
            sgs.extend(get_module_class_level_sentence_groups(module))
            pds = get_module_predicate_definitions(module)
            # get the python module name
            return Theory(
                name=module.__name__,
                predicate_definitions=list(pds.values()),
                sentence_groups=sgs,
                source_module_name=module.__name__,
            )
        if isinstance(source, (TextIOWrapper, TextIO)):
            lines = "\n".join(source.readlines())
            return self.parse(lines, file_name=file_name, **kwargs)
        raise ValueError(f"Unsupported source type: {type(source)}")

    def validate_iter(
        self, source: Union[Path, str, TextIO, ModuleType], file_name: Optional[str] = None, **kwargs
    ) -> Iterator[ValidationMessage]:
        """
        Validate a Python module

        Note that mypy is assumed to be installed.

        Example:

            >>> import tests.theorems.animals as animals
            >>> pp = PythonParser()
            >>> pp.validate(animals)
            []

        Next we try with a deliberate error:

            >>> with open(animals.__file__) as f:
            ...    prog = f.read()
            >>> print(prog)
            <BLANKLINE>
            ...
            @dataclass
            class Likes(FactMixin):
                subject: Thing
                object: Thing
            ...


            >>> prog += "\\n@axiom\\n"
            >>> prog += "def bad_axiom(x: Thing, y: int):\\n"
            >>> prog += "    assert Likes(x, y)\\n"
            >>> errs = pp.validate(prog)
            >>> assert errs
            >>> assert "incompatible type" in errs[0].message

        :param source:
        :param file_name:
        :param kwargs:
        :return:
        """
        from mypy import api

        result: Optional[Tuple] = None
        if isinstance(source, ModuleType):
            result = api.run([str(source.__file__)])
        elif isinstance(source, str):
            with tempfile.NamedTemporaryFile(mode="w+t", delete=False) as temp_file:
                temp_file.write(source)
                temp_file.flush()
                result = api.run([temp_file.name])
        elif isinstance(source, Path):
            result = api.run([str(source)])
        if result is None:
            raise ValueError(f"Unsupported source type: {type(source)}")
        stdout, stderr, exit_code = result
        if exit_code == 0:
            return
        lines = stderr.splitlines() + stdout.splitlines()
        if not lines:
            raise ValueError(f"No output from mypy; ret={exit_code}; stdout={stdout}; stderr={stderr}")
        for line in lines:
            yield ValidationMessage(line)

transform(source, **kwargs)

Transform a Python module into a Theory

Parameters:

Name Type Description Default
source ModuleType
required
kwargs
{}

Returns:

Type Description
Theory
Source code in src/typedlogic/parsers/pyparser/python_parser.py 
 94
 95
 96
 97
 98
 99
100
101
102
def transform(self, source: ModuleType, **kwargs) -> Theory:
    """
    Transform a Python module into a Theory

    :param source:
    :param kwargs:
    :return:
    """
    return translate_module_to_theory(source)

parse(source, file_name=None, **kwargs)

Parse a Python module or source code into a Theory.

Parameters:

Name Type Description Default
source Union[Path, str, TextIO, ModuleType]
required
file_name Optional[str]
None
kwargs
{}

Returns:

Type Description
Theory
Source code in src/typedlogic/parsers/pyparser/python_parser.py 
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
def parse(self, source: Union[Path, str, TextIO, ModuleType], file_name: Optional[str] = None, **kwargs) -> Theory:
    """
    Parse a Python module or source code into a Theory.

    :param source:
    :param file_name:
    :param kwargs:
    :return:
    """
    if isinstance(source, ModuleType):
        return translate_module_to_theory(source)
    if self.auto_validate:
        errs = self.validate(source)
        if errs:
            raise ValueError(f"Validation errors: {errs}")
    if isinstance(source, Path):
        with source.open() as f:
            return self.parse(f, file_name=str(source), **kwargs)
    if isinstance(source, str):
        module = compile_python(source, name=None, package_path=file_name)
        sgs = get_module_sentence_groups(source)
        sgs.extend(get_module_class_level_sentence_groups(module))
        pds = get_module_predicate_definitions(module)
        # get the python module name
        return Theory(
            name=module.__name__,
            predicate_definitions=list(pds.values()),
            sentence_groups=sgs,
            source_module_name=module.__name__,
        )
    if isinstance(source, (TextIOWrapper, TextIO)):
        lines = "\n".join(source.readlines())
        return self.parse(lines, file_name=file_name, **kwargs)
    raise ValueError(f"Unsupported source type: {type(source)}")

validate_iter(source, file_name=None, **kwargs)

Validate a Python module

Note that mypy is assumed to be installed.

Example:

>>> import tests.theorems.animals as animals
>>> pp = PythonParser()
>>> pp.validate(animals)
[]

Next we try with a deliberate error:

>>> with open(animals.__file__) as f:
...    prog = f.read()
>>> print(prog)
<BLANKLINE>
...
@dataclass
class Likes(FactMixin):
    subject: Thing
    object: Thing
...


>>> prog += "\n@axiom\n"
>>> prog += "def bad_axiom(x: Thing, y: int):\n"
>>> prog += "    assert Likes(x, y)\n"
>>> errs = pp.validate(prog)
>>> assert errs
>>> assert "incompatible type" in errs[0].message

Parameters:

Name Type Description Default
source Union[Path, str, TextIO, ModuleType]
required
file_name Optional[str]
None
kwargs
{}

Returns:

Type Description
Iterator[ValidationMessage]
Source code in src/typedlogic/parsers/pyparser/python_parser.py 
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
def validate_iter(
    self, source: Union[Path, str, TextIO, ModuleType], file_name: Optional[str] = None, **kwargs
) -> Iterator[ValidationMessage]:
    """
    Validate a Python module

    Note that mypy is assumed to be installed.

    Example:

        >>> import tests.theorems.animals as animals
        >>> pp = PythonParser()
        >>> pp.validate(animals)
        []

    Next we try with a deliberate error:

        >>> with open(animals.__file__) as f:
        ...    prog = f.read()
        >>> print(prog)
        <BLANKLINE>
        ...
        @dataclass
        class Likes(FactMixin):
            subject: Thing
            object: Thing
        ...


        >>> prog += "\\n@axiom\\n"
        >>> prog += "def bad_axiom(x: Thing, y: int):\\n"
        >>> prog += "    assert Likes(x, y)\\n"
        >>> errs = pp.validate(prog)
        >>> assert errs
        >>> assert "incompatible type" in errs[0].message

    :param source:
    :param file_name:
    :param kwargs:
    :return:
    """
    from mypy import api

    result: Optional[Tuple] = None
    if isinstance(source, ModuleType):
        result = api.run([str(source.__file__)])
    elif isinstance(source, str):
        with tempfile.NamedTemporaryFile(mode="w+t", delete=False) as temp_file:
            temp_file.write(source)
            temp_file.flush()
            result = api.run([temp_file.name])
    elif isinstance(source, Path):
        result = api.run([str(source)])
    if result is None:
        raise ValueError(f"Unsupported source type: {type(source)}")
    stdout, stderr, exit_code = result
    if exit_code == 0:
        return
    lines = stderr.splitlines() + stdout.splitlines()
    if not lines:
        raise ValueError(f"No output from mypy; ret={exit_code}; stdout={stdout}; stderr={stderr}")
    for line in lines:
        yield ValidationMessage(line)