# Copyright (C) 2023 IBM Corp.
# SPDX-License-Identifier: Apache-2.0
from . import util
__all__ = [
'EmptyTheory',
'_thy',
'enumerate_extensions',
'extend',
'lookup_axiom',
'lookup_constant',
'lookup_definition',
'lookup_extension',
'lookup_python_type_alias',
'lookup_theorem',
'lookup_type_constructor',
'new_axiom',
'new_base_type',
'new_constant',
'new_definition',
'new_python_type_alias',
'new_theorem',
'new_type_constructor',
'reset',
'settings',
'show_axioms',
'show_constants',
'show_definitions',
'show_extensions',
'show_python_type_aliases',
'show_theorems',
'show_type_constructors',
]
[docs]
def _thy(theory=None):
"""Gets `theory` or the top theory.
If `theory` is not given, assumes the top theory.
Returns:
`theory` or the top theory.
"""
from .theory import Theory
return Theory._thy(theory)
def EmptyTheory(**kwargs):
"""Creates an empty theory.
An empty theory is one containing no extensions (not even those added by
the standard prelude).
Returns:
An empty theory (:class:`Theory`).
"""
return _thy().__class__(load_prelude=False, **kwargs) # no args
# -- Adding extensions -----------------------------------------------------
[docs]
def extend(ext, theory=None):
"""Adds extension.
See :meth:`Theory.extend`.
"""
return _thy(theory).extend(ext)
[docs]
def new_base_type(arg1, theory=None, **kwargs):
"""Adds new base type.
See :meth:`Theory.new_base_type`.
"""
return _thy(theory).new_base_type(arg1, **kwargs)
[docs]
def new_type_constructor(arg1, arg2, arg3=None, theory=None, **kwargs):
"""Adds new type constructor.
See :meth:`Theory.new_type_constructor`.
"""
return _thy(theory).new_type_constructor(arg1, arg2, arg3, **kwargs)
[docs]
def new_constant(arg1, arg2, theory=None, **kwargs):
"""Adds new (primitive) constant.
See :meth:`Theory.new_constant`.
"""
return _thy(theory).new_constant(arg1, arg2, **kwargs)
[docs]
def new_axiom(arg1, arg2=None, theory=None, **kwargs):
"""Adds new axiom.
See :meth:`Theory.new_axiom`.
"""
return _thy(theory).new_axiom(arg1, arg2, **kwargs)
[docs]
def new_definition(arg1, arg2, theory=None, **kwargs):
"""Adds new definition.
See :meth:`Theory.new_definition`.
"""
return _thy(theory).new_definition(arg1, arg2, **kwargs)
[docs]
def new_theorem(arg1, arg2=None, theory=None, **kwargs):
"""Adds new theorem.
See :meth:`Theory.new_theorem`.
"""
return _thy(theory).new_theorem(arg1, arg2, **kwargs)
[docs]
def new_python_type_alias(arg1, arg2, arg3=None, theory=None, **kwargs):
"""Adds new Python type alias.
See :meth:`Theory.new_python_type_alias`.
"""
return _thy(theory).new_python_type_alias(arg1, arg2, arg3, **kwargs)[1]
# -- Removing extensions ---------------------------------------------------
[docs]
def reset(arg=None, theory=None):
"""Removes all extensions since *arg* (inclusive).
See :meth:`Theory.reset`.
"""
return _thy(theory).reset(arg)
# -- Querying extensions ---------------------------------------------------
[docs]
def enumerate_extensions(*args, theory=None, **kwargs):
"""Enumerates extensions matching criteria.
See :meth:`Theory.enumerate_extensions`.
"""
return _thy(theory).enumerate_extensions(*args, **kwargs)
[docs]
def lookup_extension(*args, theory=None, **kwargs):
"""Searches for extension.
See :meth:`Theory.lookup_extension`.
"""
return _thy(theory).lookup_extension(*args, **kwargs)
[docs]
def lookup_type_constructor(*args, theory=None, **kwargs):
"""Searches for type constructor.
See :meth:`Theory.lookup_type_constructor`.
"""
return _thy(theory).lookup_type_constructor(*args, **kwargs)
[docs]
def lookup_constant(*args, theory=None, **kwargs):
"""Searches for constant.
See :meth:`Theory.lookup_constant`.
"""
return _thy(theory).lookup_constant(*args, **kwargs)
[docs]
def lookup_axiom(*args, theory=None, **kwargs):
"""Searches for axiom.
See :meth:`Theory.lookup_axiom`.
"""
return _thy(theory).lookup_axiom(*args, **kwargs)
[docs]
def lookup_definition(*args, theory=None, **kwargs):
"""Searches for definition.
See :meth:`Theory.lookup_definition`.
"""
return _thy(theory).lookup_definition(*args, **kwargs)
[docs]
def lookup_theorem(*args, theory=None, **kwargs):
"""Searches for theorem.
See :meth:`Theory.lookup_theorem`.
"""
return _thy(theory).lookup_theorem(*args, **kwargs)
[docs]
def lookup_python_type_alias(*args, theory=None, **kwargs):
"""Searches for Python type alias.
See :meth:`Theory.lookup_python_type_alias`.
"""
return _thy(theory).lookup_python_type_alias(*args, **kwargs)
def lookup_python_type_alias_spec(*args, theory=None, **kwargs):
"""Searches for Python type alias specification.
See :meth:`Theory.lookup_python_type_alias_spec`.
"""
return _thy(theory).lookup_python_type_alias_spec(*args, **kwargs)
# -- Showing extensions ----------------------------------------------------
[docs]
def show_extensions(*args, theory=None, **kwargs):
"""Prints extensions matching criteria.
See :meth:`Theory.show_extensions`.
"""
return _thy(theory).show_extensions(*args, **kwargs)
[docs]
def show_type_constructors(*args, theory=None, **kwargs):
"""Prints type constructors matching criteria.
See :meth:`Theory.show_extensions`.
"""
thy = _thy(theory)
return thy.show_extensions(
*args, class_=thy.NewTypeConstructor, **kwargs)
[docs]
def show_constants(*args, theory=None, **kwargs):
"""Prints constants matching criteria.
See :meth:`Theory.show_extensions`.
"""
thy = _thy(theory)
return thy.show_extensions(
*args, class_=thy.NewConstant, **kwargs)
[docs]
def show_axioms(*args, theory=None, **kwargs):
"""Prints axioms matching criteria.
See :meth:`Theory.show_extensions`.
"""
thy = _thy(theory)
return thy.show_extensions(
*args, class_=thy.NewAxiom, **kwargs)
[docs]
def show_definitions(*args, theory=None, **kwargs):
"""Prints definitions matching criteria.
See :meth:`Theory.show_extensions`.
"""
thy = _thy(theory)
return thy.show_extensions(
*args, class_=thy.NewDefinition, **kwargs)
[docs]
def show_theorems(*args, theory=None, **kwargs):
"""Prints theorems matching criteria.
See :meth:`Theory.show_extensions`.
"""
thy = _thy(theory)
return thy.show_extensions(
*args, class_=thy.NewTheorem, **kwargs)
[docs]
def show_python_type_aliases(*args, theory=None, **kwargs):
"""Prints Python type aliases matching criteria.
See :meth:`Theory.show_extensions`.
"""
thy = _thy(theory)
return thy.show_extensions(
*args, class_=thy.NewPythonTypeAlias, **kwargs)
# -- Settings --------------------------------------------------------------
#: Settings table of the top theory.
settings = util.Proxy(lambda: _thy().settings)